[proofplan] The proof is a direct comparison between the section $s$ and its coordinate expression in each bundle trivialization. If $s$ is smooth, composing with a smooth trivialization and then with the smooth projection to $F$ gives a smooth local representative. Conversely, if each local representative is smooth, then locally $s$ is obtained by applying the inverse trivialization to the smooth graph map built from that representative. Since smoothness of maps between manifolds is checked locally on the domain by smooth coordinate representatives, these local smoothness statements assemble to show that $s$ is smooth on all of $M$. [/proofplan] [step:Extract the local representative from a smooth section] Assume first that $s: M \to E$ is smooth. Fix $i \in I$. For every $x \in U_i$, the section condition gives $\rho(s(x))=x \in U_i$, hence $s(x) \in \rho^{-1}(U_i)$. Since $U_i \subset M$ is open and $\rho:E \to M$ is smooth, hence continuous, the subset $\rho^{-1}(U_i) \subset E$ is open. Thus the restriction corestricts to the map $s|_{U_i}: U_i \to \rho^{-1}(U_i)$. This map is smooth by locality of smoothness under restriction to open submanifolds of the domain and codomain. The trivialization $\Phi_i: \rho^{-1}(U_i) \to U_i \times F$ is a diffeomorphism by the definition of a smooth bundle atlas, hence is smooth. Therefore the composite $\Phi_i \circ s|_{U_i}: U_i \to U_i \times F$ is smooth. Let $\operatorname{pr}_2: U_i \times F \to F$ be the second projection. The projection $\operatorname{pr}_2$ is smooth for the product smooth structure, so the composite $s_i = \operatorname{pr}_2 \circ \Phi_i \circ s|_{U_i}: U_i \to F$ is smooth. Since $i \in I$ was arbitrary, every local representative $s_i$ is smooth. [/step] [step:Reconstruct each local section from its representative] Assume conversely that for every $i \in I$ the map \begin{align*} s_i: U_i &\to F \end{align*} is smooth. Fix $i \in I$. Define the graph map \begin{align*} g_i: U_i &\to U_i \times F. \end{align*} For each $x \in U_i$, set $g_i(x)=(x,s_i(x))$. The first component of $g_i$ is the identity map $\operatorname{id}_{U_i}: U_i \to U_i$, which is smooth, and the second component is $s_i$, which is smooth by hypothesis. By the defining smoothness criterion for maps into a Product Manifold, a map into $U_i \times F$ is smooth precisely when its component maps to $U_i$ and to $F$ are smooth. Therefore $g_i$ is smooth as a map into the product manifold $U_i \times F$. Define the corestricted local section \begin{align*} \sigma_i: U_i &\to \rho^{-1}(U_i) \end{align*} by $\sigma_i(x)=s(x)$ for every $x \in U_i$. This is well-defined because the section condition gives $\rho(s(x))=x \in U_i$, hence $s(x) \in \rho^{-1}(U_i)$. Let $\operatorname{pr}_1:U_i\times F\to U_i$ be the first projection. Since $\operatorname{pr}_1 \circ \Phi_i=\rho|_{\rho^{-1}(U_i)}$, the point $\Phi_i(\sigma_i(x))$ has first component $x$. Its second component is, by definition, $s_i(x)$. Therefore \begin{align*} \Phi_i(\sigma_i(x)) = (x,s_i(x)) = g_i(x) \end{align*} for every $x \in U_i$. Thus \begin{align*} \sigma_i = \Phi_i^{-1} \circ g_i. \end{align*} The inverse trivialization $\Phi_i^{-1}: U_i \times F \to \rho^{-1}(U_i)$ is smooth because $\Phi_i$ is a diffeomorphism. Since $g_i$ is smooth, the composite $\Phi_i^{-1}\circ g_i$ is smooth as a map into $\rho^{-1}(U_i)$. The subset $\rho^{-1}(U_i) \subset E$ is open because $U_i \subset M$ is open and $\rho$ is continuous, so the inclusion map \begin{align*} j_i: \rho^{-1}(U_i) &\to E \end{align*} is smooth for the Open Submanifold structure. Hence $s|_{U_i}=j_i\circ \sigma_i=j_i\circ \Phi_i^{-1}\circ g_i: U_i \to E$ is smooth. [guided] We now explain carefully why a smooth local representative gives a smooth local section. Fix an index $i \in I$ and assume that the representative \begin{align*} s_i: U_i &\to F \end{align*} is smooth. The section condition says that for every $x \in U_i$, \begin{align*} \rho(s(x)) = x. \end{align*} The trivialization $\Phi_i$ records a point of $\rho^{-1}(U_i)$ by its base point in $U_i$ and its fibre coordinate in $F$. Let $\operatorname{pr}_1:U_i\times F\to U_i$ be the first projection. Since $\operatorname{pr}_1 \circ \Phi_i=\rho|_{\rho^{-1}(U_i)}$, applying $\Phi_i$ to $s(x)$ produces a pair whose first component is \begin{align*} \operatorname{pr}_1(\Phi_i(s(x))) = \rho(s(x)) = x. \end{align*} By the definition of the local representative, its second component is \begin{align*} \operatorname{pr}_2(\Phi_i(s(x))) = s_i(x). \end{align*} Therefore \begin{align*} \Phi_i(s(x)) = (x,s_i(x)). \end{align*} This motivates the graph map \begin{align*} g_i: U_i &\to U_i \times F. \end{align*} For each $x \in U_i$, define $g_i(x)=(x,s_i(x))$. To check that $g_i$ is smooth, use the defining smoothness criterion for maps into a Product Manifold: a map into $U_i \times F$ is smooth precisely when its component maps to $U_i$ and to $F$ are smooth. Here the first component is $\operatorname{id}_{U_i}: U_i \to U_i$, which is smooth, and the second component is $s_i: U_i \to F$, which is smooth by hypothesis. Hence $g_i$ is smooth. Define the corestricted local section \begin{align*} \sigma_i: U_i &\to \rho^{-1}(U_i) \end{align*} by $\sigma_i(x)=s(x)$ for every $x \in U_i$. This map has codomain $\rho^{-1}(U_i)$ because the section condition gives $\rho(s(x))=x \in U_i$. The equality $\Phi_i(\sigma_i(x))=g_i(x)$ for every $x \in U_i$ gives the identity of maps \begin{align*} \sigma_i = \Phi_i^{-1}\circ g_i. \end{align*} The map $\Phi_i^{-1}: U_i \times F \to \rho^{-1}(U_i)$ is smooth because $\Phi_i$ is a diffeomorphism in the smooth bundle atlas. This proves smoothness of $\sigma_i$ as a map into the open submanifold $\rho^{-1}(U_i)$. Since $U_i \subset M$ is open and $\rho$ is continuous, $\rho^{-1}(U_i) \subset E$ is open. Therefore the inclusion map \begin{align*} j_i: \rho^{-1}(U_i) &\to E \end{align*} is smooth for the Open Submanifold structure, and $s|_{U_i}=j_i\circ \sigma_i=j_i\circ \Phi_i^{-1}\circ g_i: U_i \to E$ is a composite of smooth maps. Hence $s|_{U_i}$ is smooth as a map into $E$. [/guided] [/step] [step:Assemble the local smoothness statements over the bundle atlas] We have shown that $s|_{U_i}: U_i \to E$ is smooth for every $i \in I$. Since the open sets $U_i$ cover $M$, the family $(U_i)_{i \in I}$ is an open cover of the domain $M$. By the locality of smoothness for manifold maps, smoothness of a map between smooth manifolds is local on the domain: for each point $x \in M$, choose an index $i \in I$ with $x \in U_i$; because $s|_{U_i}$ is smooth, every coordinate representative of $s$ near $x$ agrees after restricting to a smaller coordinate neighbourhood with a coordinate representative of $s|_{U_i}$. Hence the defining coordinate smoothness condition for $s$ holds at every point of $M$. Therefore $s$ is smooth on $M$. This proves the converse implication, and therefore $s$ is smooth if and only if every local representative $s_i$ is smooth. [/step]