[proofplan] Choose a local trivialization of the vector bundle near the point $p$. The inverse image of the standard basis vectors of $\mathbb{R}^k$ gives $k$ smooth local sections over that neighbourhood. Every smooth section has smooth component functions in this trivialization, which gives spanning, and fibrewise linearity of the trivialization gives uniqueness of those components. [/proofplan]

[step:Choose a local trivialization around $p$] Since $\pi: E \to M$ is a smooth vector bundle of rank $k$, there exists an open neighbourhood $U \subset M$ of $p$ and a smooth bundle trivialization \begin{align*} \Phi: E|_U \to U \times \mathbb{R}^k. \end{align*} Let $\operatorname{pr}_1: U \times \mathbb{R}^k \to U$ denote projection onto the first factor, and let $\operatorname{pr}_2: U \times \mathbb{R}^k \to \mathbb{R}^k$ denote projection onto the second factor. The trivialization satisfies $\operatorname{pr}_1 \circ \Phi = \pi|_{E|_U}$ and, for each $q \in U$, the restricted map \begin{align*} \Phi_q: E_q \to \{q\} \times \mathbb{R}^k \end{align*} is a linear isomorphism after identifying $\{q\} \times \mathbb{R}^k$ with $\mathbb{R}^k$ by $\operatorname{pr}_2|_{\{q\} \times \mathbb{R}^k}$. Let $\varepsilon_1, \dots, \varepsilon_k \in \mathbb{R}^k$ denote the standard basis vectors. For each $i \in \{1, \dots, k\}$, define the map $s_i: U \to E|_U$ by \begin{align*} s_i(q) = \Phi^{-1}(q, \varepsilon_i) \quad \text{for } q \in U. \end{align*} Because $\Phi^{-1}: U \times \mathbb{R}^k \to E|_U$ is smooth and the map $U \to U \times \mathbb{R}^k$ given by $q \mapsto (q,\varepsilon_i)$ is smooth, each $s_i$ is a smooth section of $E|_U \to U$. [/step]

[step:Express every section in the local frame]Let $s \in \Gamma(U, E|_U)$ be an arbitrary smooth section. Define the smooth map $g: U \to \mathbb{R}^k$ by \begin{align*} g(q) = \operatorname{pr}_2(\Phi(s(q))) \quad \text{for } q \in U. \end{align*} For each $i \in \{1, \dots, k\}$, let $\rho_i: \mathbb{R}^k \to \mathbb{R}$ be the $i$-th coordinate projection, and define the map $f_i: U \to \mathbb{R}$ by \begin{align*} f_i(q) = \rho_i(g(q)) \quad \text{for } q \in U. \end{align*} Then $f_i \in C^\infty(U)$ for every $i$, since $g$ and $\rho_i$ are smooth. For every $q \in U$, the definition of $g$, the coordinate expansion in $\mathbb{R}^k$, and fibrewise linearity of $\Phi_q: E_q \to \{q\} \times \mathbb{R}^k$ give \begin{align*} \Phi(s(q)) = (q, g(q)) = \left(q, \sum_{i=1}^k f_i(q)\varepsilon_i\right) = \Phi\left(\sum_{i=1}^k f_i(q)s_i(q)\right). \end{align*} Since $\Phi$ is injective, this gives \begin{align*} s = \sum_{i=1}^k f_i s_i. \end{align*} Thus $s_1,\dots,s_k$ span $\Gamma(U,E|_U)$ as a $C^\infty(U)$-module.[/step]

[guided]The purpose of the trivialization is to turn a section of $E|_U$ into an ordinary $\mathbb{R}^k$-valued smooth function. Let $s \in \Gamma(U,E|_U)$ be a smooth section. Since $s(q) \in E_q$ and $\Phi$ preserves base points, the point $\Phi(s(q))$ has first coordinate $q$. Therefore the second coordinate defines the smooth map $g: U \to \mathbb{R}^k$ given by \begin{align*} g(q) = \operatorname{pr}_2(\Phi(s(q))) \quad \text{for } q \in U. \end{align*} This map records the components of $s$ in the chosen local trivialization. To extract the scalar coefficient functions, let $\rho_i: \mathbb{R}^k \to \mathbb{R}$ be the $i$-th coordinate projection for each $i \in \{1,\dots,k\}$, and define the map $f_i: U \to \mathbb{R}$ by \begin{align*} f_i(q) = \rho_i(g(q)) \quad \text{for } q \in U. \end{align*} Because $s$, $\Phi$, $\operatorname{pr}_2$, and $\rho_i$ are smooth maps, each $f_i$ is a smooth real-valued function on $U$, so $f_i \in C^\infty(U)$. Now fix $q \in U$. In the [vector space](/page/Vector%20Space) $\mathbb{R}^k$, the vector $g(q)$ has the coordinate expansion \begin{align*} g(q)=\sum_{i=1}^k f_i(q)\varepsilon_i. \end{align*} By definition of $s_i$, we have $\Phi(s_i(q))=(q,\varepsilon_i)$. Since $\Phi$ is fibrewise linear on $E_q$, scalar multiplication and addition in the fibre are transported to scalar multiplication and addition in $\mathbb{R}^k$. Hence \begin{align*} \Phi\left(\sum_{i=1}^k f_i(q)s_i(q)\right) = \left(q,\sum_{i=1}^k f_i(q)\varepsilon_i\right) = (q,g(q)) = \Phi(s(q)). \end{align*} The map $\Phi$ is a diffeomorphism, hence injective, so \begin{align*} s(q)=\sum_{i=1}^k f_i(q)s_i(q). \end{align*} Since this holds for every $q \in U$, we obtain the section identity \begin{align*} s=\sum_{i=1}^k f_i s_i. \end{align*} Thus every smooth section is a $C^\infty(U)$-linear combination of $s_1,\dots,s_k$.[/guided]

[step:Use fibrewise linearity to prove the coefficients are unique] Suppose $f_1,\dots,f_k \in C^\infty(U)$ satisfy \begin{align*} \sum_{i=1}^k f_i s_i = 0, \end{align*} where $0: U \to E|_U$ denotes the zero section. Fix $q \in U$. Applying $\Phi$ to the equality in the fibre $E_q$ gives \begin{align*} \left(q,\sum_{i=1}^k f_i(q)\varepsilon_i\right) = \Phi(0(q)) = (q,0). \end{align*} Thus \begin{align*} \sum_{i=1}^k f_i(q)\varepsilon_i = 0 \end{align*} in $\mathbb{R}^k$. Since $\varepsilon_1,\dots,\varepsilon_k$ is the standard basis of $\mathbb{R}^k$, we have $f_i(q)=0$ for every $i \in \{1,\dots,k\}$. As $q \in U$ was arbitrary, $f_i=0$ on $U$ for every $i$. Therefore $s_1,\dots,s_k$ are $C^\infty(U)$-linearly independent. Together with the spanning result, they form a basis of $\Gamma(U,E|_U)$ as a $C^\infty(U)$-module. Hence $\Gamma(U,E|_U)$ is free of rank $k$. [/step]