[proofplan]
The evaluation map is fibrewise the [linear map](/page/Linear%20Map) sending the standard basis vectors of $\mathbb{R}^n$ to the generating sections $s_1(x),\dots,s_n(x)$, so surjectivity follows directly from the spanning hypothesis. To prove that the kernel is a vector subbundle, we work in a local trivialization of $E$ and write the sections as columns of a smooth $k\times n$ matrix of constant rank $k$. Near each point, one $k\times k$ minor is invertible, and solving the resulting linear system gives an explicit smooth local frame for the kernel. These local frames prove that $K$ has rank $n-k$, and fibrewise exactness gives the short exact sequence.
[/proofplan]
[step:Verify that the evaluation map is a smooth surjective vector bundle morphism]
Let $\pi:E\to X$ denote the vector bundle projection map, and let $p_1$ denote the projection map from $X\times \mathbb{R}^n$ to $X$. For each $x\in X$, define the fibre map $(\operatorname{ev}_s)_x$ from $\mathbb{R}^n$ to $E_x$ by
\begin{align*}
(\operatorname{ev}_s)_x(a_1,\dots,a_n)=\sum_{j=1}^n a_j s_j(x).
\end{align*}
This map is linear because addition and scalar multiplication are taken in the [vector space](/page/Vector%20Space) $E_x$. The identity
\begin{align*}
\pi(\operatorname{ev}_s(x,a))=x=p_1(x,a)
\end{align*}
for every $(x,a)\in X\times\mathbb{R}^n$ shows that $\operatorname{ev}_s$ is a vector bundle morphism over $X$ once smoothness is verified.
To check smoothness, let $(U,\varphi)$ be a vector bundle trivialization of $E$, where
\begin{align*}
\varphi:\pi^{-1}(U)&\to U\times\mathbb{R}^k
\end{align*}
is a smooth vector bundle isomorphism over $U$. For each $j\in\{1,\dots,n\}$, define the local coefficient map
\begin{align*}
\sigma_j:U&\to\mathbb{R}^k
\end{align*}
by the condition
\begin{align*}
\varphi(s_j(x))=(x,\sigma_j(x)).
\end{align*}
Since $s_j$ and $\varphi$ are smooth, each $\sigma_j$ is smooth. In the trivialization, the evaluation map is the map from $U\times\mathbb{R}^n$ to $U\times\mathbb{R}^k$ given by
\begin{align*}
(x,a_1,\dots,a_n)\mapsto \left(x,\sum_{j=1}^n a_j\sigma_j(x)\right),
\end{align*}
which is smooth. Hence $\operatorname{ev}_s$ is smooth.
For every $x\in X$, the spanning hypothesis says that $s_1(x),\dots,s_n(x)$ span $E_x$. Therefore $(\operatorname{ev}_s)_x:\mathbb{R}^n\to E_x$ is surjective. Thus $\operatorname{ev}_s:X\times\mathbb{R}^n\to E$ is a surjective smooth vector bundle morphism.
[/step]
[step:Construct local smooth frames for the kernel]
Fix $x_0\in X$. Choose a vector bundle trivialization
\begin{align*}
\varphi:\pi^{-1}(U_0)&\to U_0\times\mathbb{R}^k
\end{align*}
over an open neighbourhood $U_0\subset X$ of $x_0$. For each $j\in\{1,\dots,n\}$, let
\begin{align*}
\sigma_j:U_0&\to\mathbb{R}^k
\end{align*}
be defined by $\varphi(s_j(x))=(x,\sigma_j(x))$. Define the smooth matrix-valued map
\begin{align*}
A:U_0&\to\mathbb{R}^{k\times n}
\end{align*}
by taking $\sigma_j(x)$ as the $j$-th column of $A(x)$.
Since $s_1(x_0),\dots,s_n(x_0)$ span $E_{x_0}$, the matrix $A(x_0)$ has rank $k$. Choose a permutation $P:\mathbb{R}^n\to\mathbb{R}^n$ of the standard coordinate basis such that the first $k$ columns of $A(x_0)P$ form an invertible $k\times k$ matrix. Composing the product-bundle trivialization over $U_0$ with the smooth bundle automorphism $\operatorname{id}_{U_0}\times P$ only relabels the fibre coordinates of $U_0\times\mathbb{R}^n$, so in the following local computation we replace $A$ by $AP$ and keep the name $A$ for the relabelled matrix. Define smooth matrix-valued maps $B:U_0\to\mathbb{R}^{k\times k}$ and $C:U_0\to\mathbb{R}^{k\times(n-k)}$ by writing
\begin{align*}
A(x)=\begin{pmatrix}B(x)&C(x)\end{pmatrix}.
\end{align*}
Because $\det B(x_0)\neq 0$ and $\det B:U_0\to\mathbb{R}$ is continuous, there exists an open neighbourhood $U\subset U_0$ of $x_0$ such that $\det B(x)\neq 0$ for every $x\in U$. Hence $B(x)$ is invertible for every $x\in U$. Define the cofactor matrix map $\operatorname{Cof}:\mathbb{R}^{k\times k}\to\mathbb{R}^{k\times k}$ by the usual polynomial cofactor formulas. Since $B$ is smooth, $x\mapsto \operatorname{Cof}(B(x))$ and $x\mapsto \det B(x)$ are smooth, and $1/\det B$ is smooth on $U$ because $\det B$ has no zero on $U$. The adjugate formula gives
\begin{align*}
B(x)^{-1}=\frac{1}{\det B(x)}\operatorname{Cof}(B(x))^\top,
\end{align*}
so the map $x\mapsto B(x)^{-1}$ is smooth on $U$.
We use the convention that when $n=k$, the set $\{1,\dots,n-k\}$ is empty, $\mathbb{R}^{n-k}=\mathbb{R}^0=\{0\}$, and an empty family is a basis of the zero vector space. For each $r\in\{1,\dots,n-k\}$, let $e_r\in\mathbb{R}^{n-k}$ denote the $r$-th standard basis vector, define the relabelled-coordinate kernel vector $\tilde v_r:U\to\mathbb{R}^n$ by
\begin{align*}
\tilde v_r(x)=\left(-B(x)^{-1}C(x)e_r,\ e_r\right),
\end{align*}
where we use the splitting $\mathbb{R}^n=\mathbb{R}^k\oplus\mathbb{R}^{n-k}$, and define the original-coordinate kernel vector $v_r:U\to\mathbb{R}^n$ by $v_r(x):=P\tilde v_r(x)$. Each $v_r$ is smooth. Moreover,
\begin{align*}
A(x)P^{-1}v_r(x)=A(x)\tilde v_r(x)=B(x)\left(-B(x)^{-1}C(x)e_r\right)+C(x)e_r=0.
\end{align*}
Therefore $(x,v_r(x))\in K$ for every $x\in U$ in the original product-bundle coordinates.
We now show that $v_1(x),\dots,v_{n-k}(x)$ form a basis of the original-coordinate kernel $\ker(A(x)P^{-1})$ for each $x\in U$. Let $a\in\mathbb{R}^n$, define $\tilde a:=P^{-1}a$, and write $\tilde a=(u,w)$ with $u\in\mathbb{R}^k$ and $w\in\mathbb{R}^{n-k}$. Then $A(x)P^{-1}a=0$ is equivalent to $A(x)\tilde a=0$, hence to $B(x)u+C(x)w=0$, and since $B(x)$ is invertible this is equivalent to
\begin{align*}
u=-B(x)^{-1}C(x)w.
\end{align*}
Writing $w=\sum_{r=1}^{n-k}w_r e_r$, where $w_r\in\mathbb{R}$ is the $r$-th coordinate of $w$, gives
\begin{align*}
a=P\tilde a=\sum_{r=1}^{n-k}w_r P\tilde v_r(x)=\sum_{r=1}^{n-k}w_r v_r(x).
\end{align*}
The vectors $v_1(x),\dots,v_{n-k}(x)$ are linearly independent because $P^{-1}v_1(x),\dots,P^{-1}v_{n-k}(x)$ have last $n-k$ coordinates equal to the standard basis vectors $e_1,\dots,e_{n-k}$. Thus they form a basis of $\ker(A(x)P^{-1})$, which is the kernel of the original local evaluation matrix.
[guided]
Fix a point $x_0\in X$. The goal is to show that, near $x_0$, the kernel does not vary irregularly: it should be spanned by $n-k$ smooth vector-valued functions. Choose a vector bundle trivialization
\begin{align*}
\varphi:\pi^{-1}(U_0)&\to U_0\times\mathbb{R}^k
\end{align*}
over an open neighbourhood $U_0\subset X$ of $x_0$. In this trivialization, each section $s_j:X\to E$ becomes a smooth coefficient map
\begin{align*}
\sigma_j:U_0&\to\mathbb{R}^k
\end{align*}
defined by
\begin{align*}
\varphi(s_j(x))=(x,\sigma_j(x)).
\end{align*}
Package these coefficient vectors into the smooth matrix-valued map
\begin{align*}
A:U_0&\to\mathbb{R}^{k\times n},
\end{align*}
where the $j$-th column of $A(x)$ is $\sigma_j(x)$.
The spanning hypothesis says that $s_1(x_0),\dots,s_n(x_0)$ span the $k$-dimensional vector space $E_{x_0}$. In the chosen trivialization, this is exactly the statement that the columns of $A(x_0)$ span $\mathbb{R}^k$, so $A(x_0)$ has rank $k$. Therefore at least one $k\times k$ minor of $A(x_0)$ has nonzero determinant. Choose a permutation $P:\mathbb{R}^n\to\mathbb{R}^n$ of the standard coordinate basis so that this invertible minor becomes the first $k$ columns of $A(x_0)P$. This permutation is implemented on the local product bundle $U_0\times\mathbb{R}^n$ by the smooth bundle automorphism $\operatorname{id}_{U_0}\times P$. After composing the local fibre coordinates with this automorphism, we relabel $AP$ as $A$. With this relabelled matrix, write
\begin{align*}
A(x)=\begin{pmatrix}B(x)&C(x)\end{pmatrix},
\end{align*}
where $B:U_0\to\mathbb{R}^{k\times k}$ and $C:U_0\to\mathbb{R}^{k\times(n-k)}$ are smooth matrix-valued maps. Since $\det B(x_0)\neq 0$ and $\det B$ is continuous, we may shrink to an open neighbourhood $U\subset U_0$ of $x_0$ such that $\det B(x)\neq 0$ for all $x\in U$. Thus $B(x)$ is invertible for every $x\in U$. To see directly that $x\mapsto B(x)^{-1}$ is smooth, define the cofactor matrix map $\operatorname{Cof}:\mathbb{R}^{k\times k}\to\mathbb{R}^{k\times k}$ by the usual cofactor formulas. Each entry of $\operatorname{Cof}(M)$ is a polynomial in the entries of the matrix $M\in\mathbb{R}^{k\times k}$, and $\det M$ is also polynomial in the entries of $M$. Therefore $x\mapsto \operatorname{Cof}(B(x))$ and $x\mapsto \det B(x)$ are smooth. Since $\det B(x)\neq 0$ for every $x\in U$, the reciprocal $x\mapsto 1/\det B(x)$ is smooth on $U$. The adjugate formula gives
\begin{align*}
B(x)^{-1}=\frac{1}{\det B(x)}\operatorname{Cof}(B(x))^\top,
\end{align*}
so $x\mapsto B(x)^{-1}$ is smooth on $U$.
Now solve the equation $A(x)a=0$ in these relabelled fibre coordinates. When $n=k$, we use the standard convention $\mathbb{R}^{n-k}=\mathbb{R}^0=\{0\}$ and the empty family is a basis of the zero vector space; the formulas below then contain no vectors $\tilde v_r$ and no free coordinates. For $n\ge k$ in general, write a vector $a\in\mathbb{R}^n$ as $a=(u,w)$ with $u\in\mathbb{R}^k$ and $w\in\mathbb{R}^{n-k}$, using the splitting $\mathbb{R}^n=\mathbb{R}^k\oplus\mathbb{R}^{n-k}$. Write a vector $a\in\mathbb{R}^n$ as $a=(u,w)$ with $u\in\mathbb{R}^k$ and $w\in\mathbb{R}^{n-k}$, using the splitting $\mathbb{R}^n=\mathbb{R}^k\oplus\mathbb{R}^{n-k}$. Then $A(x)a=0$ is equivalent to $B(x)u+C(x)w=0$, and since $B(x)$ is invertible this is equivalent to
\begin{align*}
u=-B(x)^{-1}C(x)w.
\end{align*}
This computation shows that the free variables are exactly the coordinates of $w\in\mathbb{R}^{n-k}$. For each $r\in\{1,\dots,n-k\}$, let $e_r\in\mathbb{R}^{n-k}$ be the $r$-th standard basis vector, define the relabelled-coordinate vector $\tilde v_r:U\to\mathbb{R}^n$ by
\begin{align*}
\tilde v_r(x)=\left(-B(x)^{-1}C(x)e_r,\ e_r\right),
\end{align*}
and define the original-coordinate vector $v_r:U\to\mathbb{R}^n$ by $v_r(x):=P\tilde v_r(x)$. Each $v_r$ is smooth because it is built from the smooth maps $B^{-1}$ and $C$ by matrix multiplication and the fixed linear map $P$. Also,
\begin{align*}
A(x)P^{-1}v_r(x)=A(x)\tilde v_r(x)=B(x)\left(-B(x)^{-1}C(x)e_r\right)+C(x)e_r=0,
\end{align*}
so $(x,v_r(x))$ lies in the kernel over $x$ in the original local product-bundle coordinates.
Finally, if $a\in\ker(A(x)P^{-1})$, define $\tilde a:=P^{-1}a$ and write $\tilde a=(u,w)$. Then $A(x)\tilde a=0$, so the equation above forces $u=-B(x)^{-1}C(x)w$. Writing
\begin{align*}
w=\sum_{r=1}^{n-k}w_r e_r
\end{align*}
with $w_r\in\mathbb{R}$ gives
\begin{align*}
a=P\tilde a=\sum_{r=1}^{n-k}w_r P\tilde v_r(x)=\sum_{r=1}^{n-k}w_r v_r(x).
\end{align*}
The vectors $v_1(x),\dots,v_{n-k}(x)$ are linearly independent because applying $P^{-1}$ sends them to vectors whose last $n-k$ coordinates are $e_1,\dots,e_{n-k}$. Hence they form a basis of $\ker(A(x)P^{-1})$ for every $x\in U$, which is exactly the local kernel in the original product-bundle coordinates.
[/guided]
[/step]
[step:Identify the locally framed kernel as a smooth vector subbundle]
For the neighbourhood $U\subset X$ constructed above, define the map $\Psi:U\times\mathbb{R}^{n-k}\to K|_U$ by
\begin{align*}
\Psi\left(x,w_1,\dots,w_{n-k}\right)=\left(x,\sum_{r=1}^{n-k}w_r v_r(x)\right),
\end{align*}
where $K|_U:=K\cap(U\times\mathbb{R}^n)$. The previous step shows that, for each $x\in U$, the vectors $v_1(x),\dots,v_{n-k}(x)$ form a basis of the fibre
\begin{align*}
K_x:=K\cap(\{x\}\times\mathbb{R}^n).
\end{align*}
Therefore $\Psi$ is fibrewise linear and bijective.
The map $\Psi$ is smooth because the maps $v_r:U\to\mathbb{R}^n$ are smooth. Its inverse is also smooth in the relabelled local coordinates: if $(x,a)\in K|_U$ and $a=(u,w)$ under $\mathbb{R}^n=\mathbb{R}^k\oplus\mathbb{R}^{n-k}$, then
\begin{align*}
\Psi^{-1}(x,a)=(x,w).
\end{align*}
This is the restriction of the smooth projection $U\times\mathbb{R}^n\to U\times\mathbb{R}^{n-k}$ after the fixed smooth coordinate permutation $P^{-1}$ used above. Thus $\Psi$ is a smooth vector bundle trivialization of $K|_U$.
Since every point $x_0\in X$ admits such a neighbourhood $U$, the subset $K\subset X\times\mathbb{R}^n$ is a smooth vector subbundle of rank $n-k$.
[/step]
[step:Check exactness fibre by fibre]
Let
\begin{align*}
\iota:K&\to X\times\mathbb{R}^n
\end{align*}
be the inclusion map. Since $K$ is a smooth vector subbundle, $\iota$ is a smooth injective vector bundle morphism. By definition of $K$, we have
\begin{align*}
\operatorname{im}\iota=\ker(\operatorname{ev}_s).
\end{align*}
The first step showed that $\operatorname{ev}_s$ is a surjective smooth vector bundle morphism. Therefore, for every $x\in X$, the fibre sequence
\begin{align*}
0\longrightarrow K_x\longrightarrow \mathbb{R}^n\xrightarrow{(\operatorname{ev}_s)_x}E_x\longrightarrow 0
\end{align*}
is an exact sequence of vector spaces. Hence
\begin{align*}
0\longrightarrow K\longrightarrow X\times\mathbb{R}^n\xrightarrow{\operatorname{ev}_s}E\longrightarrow 0
\end{align*}
is a short exact sequence of smooth vector bundles over $X$.
[/step]