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

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