[proofplan]
A vector bundle isomorphism to the product bundle transports the standard basis of $\mathbb{R}^k$ to $k$ smooth global sections of $E$, and fibrewise linearity makes those sections a basis in every fibre. Conversely, a global frame gives a fibrewise [linear map](/page/Linear%20Map) from $M \times \mathbb{R}^k$ to $E$ by taking linear combinations of the frame vectors. The only point requiring verification is smoothness of this map and of its inverse; this is checked in local bundle trivializations, where the frame becomes a smooth invertible matrix-valued function.
[/proofplan]
[step:Pull back the standard basis along a bundle trivialization]
Assume first that there is a smooth vector bundle isomorphism
\begin{align*}
\Psi:E \to M \times \mathbb{R}^k
\end{align*}
over $M$, meaning $\operatorname{pr}_1 \circ \Psi=\pi$ and each fibre map
\begin{align*}
\Psi_x:E_x \to \{x\}\times \mathbb{R}^k
\end{align*}
is a linear isomorphism. Let $u_1,\dots,u_k \in \mathbb{R}^k$ denote the standard basis. For each $i \in \{1,\dots,k\}$, define a map
\begin{align*}
e_i:M \to E, \qquad e_i(x):=\Psi^{-1}(x,u_i).
\end{align*}
Since the map $x \mapsto (x,u_i)$ is a smooth section of the product bundle and $\Psi^{-1}:M\times \mathbb{R}^k \to E$ is smooth, each $e_i$ is a smooth section of $E$.
For every $x \in M$, the vectors $(x,u_1),\dots,(x,u_k)$ form a basis of the fibre $\{x\}\times \mathbb{R}^k$. Since $\Psi_x:E_x \to \{x\}\times\mathbb{R}^k$ is a linear isomorphism, their inverse images $e_1(x),\dots,e_k(x)$ form a basis of $E_x$. Thus $e_1,\dots,e_k$ are a global frame.
[/step]
[step:Use a global frame to define a fibrewise linear map from the product bundle]
Conversely, suppose that $e_1,\dots,e_k:M \to E$ are smooth global sections such that $e_1(x),\dots,e_k(x)$ form a basis of $E_x$ for every $x \in M$. Define a map
\begin{align*}
\Phi:M \times \mathbb{R}^k \to E, \qquad \Phi(x,a):=\sum_{i=1}^k a_i e_i(x),
\end{align*}
where $a=(a_1,\dots,a_k) \in \mathbb{R}^k$ and the sum is taken in the [vector space](/page/Vector%20Space) $E_x$.
The map $\Phi$ lies over $M$, because $\pi(e_i(x))=x$ for each section $e_i$, hence
\begin{align*}
\pi(\Phi(x,a))=x=\operatorname{pr}_1(x,a).
\end{align*}
For each fixed $x \in M$, the fibre map
\begin{align*}
\Phi_x:\mathbb{R}^k \to E_x, \qquad \Phi_x(a):=\sum_{i=1}^k a_i e_i(x)
\end{align*}
is linear. Since $e_1(x),\dots,e_k(x)$ is a basis of $E_x$, the map $\Phi_x$ is a linear isomorphism.
[/step]
[step:Check smoothness and construct the smooth inverse in local trivializations]
It remains to prove that $\Phi$ is a smooth diffeomorphism of total spaces with smooth fibrewise-linear inverse. Let $p \in M$. Choose an open neighbourhood $U \subset M$ of $p$ and a smooth bundle trivialization
\begin{align*}
\tau:\pi^{-1}(U) \to U \times \mathbb{R}^k
\end{align*}
over $U$. Let $\operatorname{pr}_2:U\times\mathbb{R}^k\to\mathbb{R}^k$ denote the second projection. For each $i \in \{1,\dots,k\}$, define the smooth coordinate vector map
\begin{align*}
v_i:U \to \mathbb{R}^k, \qquad v_i(x):=\operatorname{pr}_2(\tau(e_i(x))).
\end{align*}
Define the matrix-valued map
\begin{align*}
A:U &\to \mathbb{R}^{k\times k}
\end{align*}
by taking $v_i(x)$ as the $i$-th column of $A(x)$. Since each $v_i$ is smooth, every entry of $A$ is smooth.
In the trivialization $\tau$, the map $\Phi$ is represented by
\begin{align*}
U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,a) \mapsto (x,A(x)a).
\end{align*}
This map is smooth because its coordinate functions are finite sums of products of smooth functions. For every $x \in U$, the vectors $e_1(x),\dots,e_k(x)$ form a basis of $E_x$, so their coordinate vectors $v_1(x),\dots,v_k(x)$ form a basis of $\mathbb{R}^k$. Hence $A(x) \in GL(k,\mathbb{R})$.
The local inverse is represented in the same trivialization by
\begin{align*}
U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,b) \mapsto (x,A(x)^{-1}b).
\end{align*}
The entries of $A(x)^{-1}$ are given by the cofactor formula divided by $\det A(x)$. Since the entries of $A$ are smooth and $\det A(x)\neq 0$ for all $x \in U$, the entries of $A^{-1}$ are smooth on $U$. Therefore the local inverse is smooth.
[guided]
The main issue in the converse direction is not fibrewise bijectivity; the frame hypothesis already gives that. The point is to verify smoothness of both the map and its inverse as maps between manifolds.
Fix $p \in M$ and choose an open neighbourhood $U \subset M$ of $p$ together with a smooth bundle trivialization
\begin{align*}
\tau:\pi^{-1}(U) \to U \times \mathbb{R}^k
\end{align*}
over $U$. This means that $\tau$ identifies every fibre $E_x$ with $\{x\}\times\mathbb{R}^k$ by a linear isomorphism, smoothly in $x$.
Let $\operatorname{pr}_2:U\times\mathbb{R}^k\to\mathbb{R}^k$ denote the second projection. For each frame section $e_i:M \to E$, define its coordinate vector in this trivialization by
\begin{align*}
v_i:U \to \mathbb{R}^k, \qquad v_i(x):=\operatorname{pr}_2(\tau(e_i(x))).
\end{align*}
The map $v_i$ is smooth because $e_i$ is smooth, $\tau$ is smooth, and $\operatorname{pr}_2$ is smooth. Now define
\begin{align*}
A:U &\to \mathbb{R}^{k\times k}
\end{align*}
by declaring that the $i$-th column of $A(x)$ is $v_i(x)$. Thus $A(x)$ records the frame vectors in the local trivialization.
In these coordinates, the map $\Phi$ becomes
\begin{align*}
U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,a) \mapsto (x,A(x)a).
\end{align*}
Indeed, if $a=(a_1,\dots,a_k)$, then linearity of the fibre map induced by $\tau$ gives
\begin{align*}
\tau\left(\sum_{i=1}^k a_i e_i(x)\right)
=
\left(x,\sum_{i=1}^k a_i v_i(x)\right)
=
(x,A(x)a).
\end{align*}
This coordinate expression is smooth because each component is a finite sum of products of smooth functions.
We must also show that the inverse is smooth. For each $x \in U$, the vectors $e_1(x),\dots,e_k(x)$ form a basis of $E_x$. Since $\tau$ is fibrewise linear and invertible, the coordinate vectors $v_1(x),\dots,v_k(x)$ form a basis of $\mathbb{R}^k$. Therefore $A(x)$ is an invertible matrix, so $A(x)\in GL(k,\mathbb{R})$.
The inverse coordinate map must solve $b=A(x)a$ for $a$, so it is
\begin{align*}
U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,b) \mapsto (x,A(x)^{-1}b).
\end{align*}
The entries of $A(x)^{-1}$ are smooth functions of $x$: by the cofactor formula, each entry is a polynomial in the entries of $A(x)$ divided by $\det A(x)$, and $\det A(x)$ never vanishes on $U$. Hence the inverse coordinate map is smooth. Since this argument works around every point $p \in M$, $\Phi$ is a smooth map with smooth inverse globally.
[/guided]
[/step]
[step:Conclude that the frame map is a vector bundle isomorphism]
The preceding step shows that $\Phi:M\times\mathbb{R}^k \to E$ is a smooth bijection with smooth inverse. The second step shows that $\Phi$ lies over $M$ and is linear on every fibre. Hence $\Phi$ is a smooth vector bundle isomorphism from the product bundle $\operatorname{pr}_1:M\times\mathbb{R}^k \to M$ onto $\pi:E\to M$. This proves that $E$ is trivial whenever it admits a global frame, and together with the first direction establishes the equivalence.
[/step]