[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.
[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]
[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]
