[proofplan] We prove both implications by translating between product bundle isomorphisms and global frames, using the empty-frame convention when $k=0$. If the bundle is isomorphic to the product bundle, the images of the constant standard basis sections under a chosen product isomorphism give a global smooth frame. Conversely, a global smooth frame defines a fibrewise [linear map](/page/Linear%20Map) from $M\times \mathbb{R}^k$ to $E$ by taking linear combinations of the frame vectors. Local product charts turn this map into multiplication by a smooth matrix whose determinant is nowhere zero, so the map and its inverse are smooth. [/proofplan]

[step:Pull back the standard basis sections from a product isomorphism] Assume that the smooth vector bundle $E\to M$ is isomorphic to the product vector bundle $M\times\mathbb{R}^k\to M$. Thus there exists a smooth vector bundle isomorphism \begin{align*} \Theta:M\times \mathbb{R}^k &\to E \end{align*} covering $\operatorname{id}_M$, whose restriction \begin{align*} \Theta_x:\{x\}\times \mathbb{R}^k &\to E_x \end{align*} is a linear isomorphism for every $x\in M$. Let $e_1,\dots,e_k$ denote the standard basis of $\mathbb{R}^k$. For each $j\in\{1,\dots,k\}$, define the smooth section $\sigma_j:M\to M\times \mathbb{R}^k$ by \begin{align*} \sigma_j(x)=(x,e_j). \end{align*} Define $s_j:M\to E$ by \begin{align*} s_j(x)=\Theta(\sigma_j(x)). \end{align*} Since $\sigma_j$ and $\Theta$ are smooth, each $s_j$ is smooth. Also \begin{align*} \pi(s_j(x))=\pi(\Theta(x,e_j))=x, \end{align*} so $s_j\in\Gamma(E)$ is a smooth section of $E\to M$. For each $x\in M$, the list $s_1(x),\dots,s_k(x)$ is the image under the linear isomorphism $\Theta_x$ of the standard basis $e_1,\dots,e_k$, hence is a basis of $E_x$. [/step]

[step:Use a global frame to define a fibrewise linear candidate product isomorphism] Conversely, assume that there exist smooth sections $s_1,\dots,s_k\in\Gamma(E)$ such that $s_1(x),\dots,s_k(x)$ is a basis of $E_x$ for every $x\in M$. Define the map $\Phi:M\times \mathbb{R}^k\to E$ by \begin{align*} \Phi(x,a_1,\dots,a_k)=\sum_{j=1}^k a_j s_j(x). \end{align*} The sum is taken in the [vector space](/page/Vector%20Space) $E_x$, since each $s_j(x)\in E_x$. Hence \begin{align*} \pi(\Phi(x,a_1,\dots,a_k))=x, \end{align*} so $\Phi$ covers $\operatorname{id}_M$. For every $x\in M$, define the restriction $\Phi_x:\{x\}\times \mathbb{R}^k\to E_x$ by \begin{align*} \Phi_x(x,a_1,\dots,a_k)=\sum_{j=1}^k a_j s_j(x). \end{align*} This map is linear and bijective because $s_1(x),\dots,s_k(x)$ is a basis of $E_x$. [/step]

[step:Verify smoothness of the frame map in local product charts]We prove that $\Phi$ is smooth by checking it in local product charts for the target bundle over open sets covering $M$. Let $U\subset M$ be an [open set](/page/Open%20Set) over which $E$ admits such a chart, and let \begin{align*} \tau:\pi^{-1}(U) &\to U\times \mathbb{R}^k \end{align*} be a smooth local vector bundle product chart over $U$. For each $j\in\{1,\dots,k\}$, define smooth coordinate functions \begin{align*} b_{ij}:U &\to \mathbb{R}, \qquad i\in\{1,\dots,k\}, \end{align*} by the identity \begin{align*} \tau(s_j(x))=\left(x,(b_{1j}(x),\dots,b_{kj}(x))\right). \end{align*} Let \begin{align*} A_U:U &\to \mathbb{R}^{k\times k} \end{align*} be the matrix-valued smooth map whose $(i,j)$ entry is $b_{ij}$. Then, for $(x,a)\in U\times\mathbb{R}^k$ with $a=(a_1,\dots,a_k)$, \begin{align*} \tau(\Phi(x,a))=\left(x,A_U(x)a\right). \end{align*} The map $(x,a)\mapsto (x,A_U(x)a)$ is smooth, so $\Phi$ is smooth on $U\times\mathbb{R}^k$. Since such open sets $U$ cover $M$, the map $\Phi$ is smooth. If $k=0$, the same argument uses the unique $0\times 0$ matrix, with determinant convention equal to $1$, and the empty list is the basis of the zero-dimensional fibre.[/step]

[guided]We need to check smoothness of $\Phi$ as a map into the total space $E$. Smoothness into the manifold $E$ can be checked after composing with local bundle charts whose domains cover the target over open sets covering $M$. Therefore we work over an arbitrary open set $U\subset M$ admitting a local product chart. Choose a smooth local vector bundle product chart \begin{align*} \tau:\pi^{-1}(U) &\to U\times \mathbb{R}^k. \end{align*} Inside this local product chart, each section $s_j$ becomes an ordinary smooth $\mathbb{R}^k$-valued function. More precisely, for every $j\in\{1,\dots,k\}$, define functions \begin{align*} b_{ij}:U &\to \mathbb{R}, \qquad i\in\{1,\dots,k\}, \end{align*} by requiring \begin{align*} \tau(s_j(x))=\left(x,(b_{1j}(x),\dots,b_{kj}(x))\right). \end{align*} These functions are smooth because $s_j:U\to E$ is smooth and $\tau:\pi^{-1}(U)\to U\times\mathbb{R}^k$ is smooth. Now collect these coordinate functions into a matrix-valued map \begin{align*} A_U:U &\to \mathbb{R}^{k\times k}, \end{align*} where the $(i,j)$ entry of $A_U(x)$ is $b_{ij}(x)$. The $j$th column of $A_U(x)$ is exactly the coordinate vector of $s_j(x)$ in the product chart $\tau$. For $a=(a_1,\dots,a_k)\in\mathbb{R}^k$, linearity of $\tau$ on each fibre gives first \begin{align*} \tau(\Phi(x,a))=\tau\left(\sum_{j=1}^k a_j s_j(x)\right). \end{align*} Because $\tau$ is fibrewise linear over $U$, this equals the coordinate expression \begin{align*} \left(x,\sum_{j=1}^k a_j(b_{1j}(x),\dots,b_{kj}(x))\right). \end{align*} By the definition of the matrix $A_U(x)$, the same vector is \begin{align*} \left(x,A_U(x)a\right). \end{align*} Therefore \begin{align*} \tau(\Phi(x,a))=\left(x,A_U(x)a\right). \end{align*} Thus, in the local product coordinates determined by $\tau$, the map $\Phi$ is represented by the map $U\times\mathbb{R}^k\to U\times\mathbb{R}^k$ given by \begin{align*} (x,a)\mapsto (x,A_U(x)a). \end{align*} This map is smooth because the entries of $A_U(x)$ are smooth functions of $x$ and matrix multiplication is polynomial in the entries of $A_U(x)$ and the coordinates of $a$. Since the open sets $U$ with local product charts cover $M$, $\Phi$ is smooth on all of $M\times\mathbb{R}^k$.[/guided]

[step:Construct the smooth inverse from the inverse frame matrix] If $k=0$, then $M\times\mathbb{R}^0\to M$ and $E\to M$ have zero-dimensional fibres, each fibre map $\Phi_x$ is the unique linear map between zero-dimensional vector spaces, and the local representative of the inverse is the identity map $U\times\mathbb{R}^0\to U\times\mathbb{R}^0$, hence is smooth. Assume now that $k\geq 1$. Let $GL(k,\mathbb{R})$ denote the group of invertible real $k\times k$ matrices. For each $x\in U$, the columns of $A_U(x)$ are the coordinates of the basis $s_1(x),\dots,s_k(x)$ of $E_x$, so $A_U(x)\in GL(k,\mathbb{R})$. Equivalently, \begin{align*} \det A_U(x)\neq 0 \end{align*} for every $x\in U$. Since each fibre map $\Phi_x$ is bijective and $\Phi$ covers $\operatorname{id}_M$, these fibrewise inverses assemble into a globally defined set-theoretic inverse $\Phi^{-1}:E\to M\times\mathbb{R}^k$. The local representative of $\Phi^{-1}$ over $U$ is therefore the map $U\times\mathbb{R}^k\to U\times\mathbb{R}^k$ given by \begin{align*} (x,v)\mapsto (x,A_U(x)^{-1}v). \end{align*} Let $\operatorname{adj}(B)$ denote the adjugate matrix of a square matrix $B\in\mathbb{R}^{k\times k}$, whose $(i,j)$ entry is the $(j,i)$ cofactor of $B$. Each entry of $A_U(x)^{-1}$ is smooth because \begin{align*} A_U(x)^{-1}=\frac{1}{\det A_U(x)}\operatorname{adj}(A_U(x)), \end{align*} the entries of $\operatorname{adj}(A_U(x))$ are polynomial functions of the entries of $A_U(x)$, and $\det A_U(x)$ is nowhere zero. Hence $\Phi^{-1}$ is smooth locally over every open set $U$ with a local product chart, and therefore $\Phi^{-1}$ is smooth globally. [/step]

[step:Conclude that the frame map is a vector bundle isomorphism] The map \begin{align*} \Phi:M\times\mathbb{R}^k &\to E \end{align*} is smooth, covers $\operatorname{id}_M$, is linear on each fibre, is bijective on each fibre, and has smooth inverse. Therefore $\Phi$ is a smooth vector bundle isomorphism from the product bundle $M\times\mathbb{R}^k\to M$ to $E\to M$. This proves that $E$ is isomorphic to a product bundle. Combining this with the first implication proves the equivalence. [/step]