[proofplan] Choose an ordered basis of the ambient space $V$ and write $n=\dim_k V$. We first prove directly that no linearly independent list in $V$ can have more than $n$ vectors, reducing through coordinates to the elementary statement for $k^n$. Then we construct a basis of $W$ by repeatedly adding a vector outside the span; the preceding bound forces this process to stop after finitely many steps. Finally, if $\dim_k W=\dim_k V$, the same basis-size bound shows that a basis of $W$ already spans all of $V$. [/proofplan]

[step:Bound the length of linearly independent lists in $V$ by $\dim_k V$]Let $n=\dim_k V$, and choose an ordered basis $\mathcal{B}=(v_1,\ldots,v_n)$ of $V$. If $n=0$, then $V=\{0\}$, so there are no nonempty linearly independent lists in $V$. Assume $n\geq 1$. We prove that every linearly independent list in $V$ has length at most $n$. Let $(u_1,\ldots,u_m)$ be a list of vectors in $V$ with $m>n$. By [citetheorem:9921], the coordinate map \begin{align*} \Phi_{\mathcal{B}}:V &\to k^n \end{align*} is a linear isomorphism. It is therefore enough to prove that the list $(\Phi_{\mathcal{B}}(u_1),\ldots,\Phi_{\mathcal{B}}(u_m))$ is linearly dependent in $k^n$, because applying the inverse map $\Phi_{\mathcal{B}}^{-1}:k^n\to V$ to a nontrivial linear relation gives a nontrivial linear relation among $(u_1,\ldots,u_m)$. [claim:No list of more than $n$ vectors in $k^n$ is linearly independent] Let $n\in\mathbb{N}$. If $m>n$, then every list $(x_1,\ldots,x_m)$ of vectors in $k^n$ is linearly dependent. [/claim] [proof] We prove the claim by induction on $n$. For $n=1$, write each vector $x_j\in k^1$ as $x_j=(a_j)$ with $a_j\in k$. If all $a_j=0$, then $x_1=0$, so the list is linearly dependent. Otherwise choose an index $r$ with $a_r\neq 0$. Since $m>1$, choose an index $s\neq r$. Then \begin{align*} a_s x_r-a_r x_s=0. \end{align*} The coefficients $a_s$ and $-a_r$ are not both zero because $a_r\neq 0$, so this is a nontrivial linear relation. Thus every list of more than one vector in $k^1$ is linearly dependent. Assume the statement holds for $k^{n-1}$, where $n\geq 2$. Let $(x_1,\ldots,x_m)$ be a list in $k^n$ with $m>n$. Write each vector as \begin{align*} x_j=(a_{1j},a_{2j},\ldots,a_{nj}) \end{align*} with $a_{ij}\in k$. If $x_j=0$ for some $j$, then the list is linearly dependent. Hence assume every $x_j$ is nonzero. If all first coordinates $a_{1j}$ are zero, define a projection map \begin{align*} \pi:k^n &\to k^{n-1} \end{align*} \begin{align*} (b_1,\ldots,b_n) &\mapsto (b_2,\ldots,b_n). \end{align*} Then $(\pi(x_1),\ldots,\pi(x_m))$ is a list of $m>n>n-1$ vectors in $k^{n-1}$. By the induction hypothesis, there are scalars $c_1,\ldots,c_m\in k$, not all zero, such that \begin{align*} \sum_{j=1}^m c_j\pi(x_j)=0. \end{align*} Since each first coordinate of $x_j$ is zero, the same coefficients also satisfy \begin{align*} \sum_{j=1}^m c_jx_j=0. \end{align*} Thus the original list is linearly dependent. It remains to handle the case in which some first coordinate is nonzero. After reindexing the list, assume $a_{11}\neq 0$. For each $j\in\{2,\ldots,m\}$, define \begin{align*} y_j=x_j-\frac{a_{1j}}{a_{11}}x_1. \end{align*} The first coordinate of $y_j$ is \begin{align*} a_{1j}-\frac{a_{1j}}{a_{11}}a_{11}=0. \end{align*} Let \begin{align*} \pi:k^n &\to k^{n-1} \end{align*} \begin{align*} (b_1,\ldots,b_n) &\mapsto (b_2,\ldots,b_n) \end{align*} be the projection deleting the first coordinate. The list $(\pi(y_2),\ldots,\pi(y_m))$ has $m-1>n-1$ vectors in $k^{n-1}$, so the induction hypothesis gives scalars $c_2,\ldots,c_m\in k$, not all zero, such that \begin{align*} \sum_{j=2}^m c_j\pi(y_j)=0. \end{align*} Because every $y_j$ has first coordinate zero, this implies \begin{align*} \sum_{j=2}^m c_jy_j=0. \end{align*} Substituting the definition of $y_j$ gives \begin{align*} \sum_{j=2}^m c_jx_j-\left(\sum_{j=2}^m c_j\frac{a_{1j}}{a_{11}}\right)x_1=0. \end{align*} This is a nontrivial linear relation among $x_1,\ldots,x_m$, because at least one of the coefficients $c_2,\ldots,c_m$ is nonzero. Hence $(x_1,\ldots,x_m)$ is linearly dependent. [/proof] Applying the claim to the coordinate vectors in $k^n$, every list of more than $n$ vectors in $V$ is linearly dependent. Therefore every linearly independent list in $V$ has length at most $n$.[/step]

[guided]The point of this step is to isolate the only place where the finite dimension of $V$ is used. Since $V$ has an ordered basis $\mathcal{B}=(v_1,\ldots,v_n)$, the coordinate map \begin{align*} \Phi_{\mathcal{B}}:V &\to k^n \end{align*} is a linear isomorphism by [citetheorem:9921]. A linear isomorphism preserves linear relations in both directions: if \begin{align*} \sum_{j=1}^m c_j\Phi_{\mathcal{B}}(u_j)=0 \end{align*} with some coefficient $c_j\neq 0$, then applying $\Phi_{\mathcal{B}}^{-1}$ gives \begin{align*} \sum_{j=1}^m c_ju_j=0. \end{align*} Thus it suffices to prove the corresponding fact in $k^n$. We prove that fact by induction on $n$. In $k^1$, any two vectors are scalar multiples in the following explicit sense. If $x_r=(a_r)$ has $a_r\neq 0$ and $x_s=(a_s)$ is another vector, then \begin{align*} a_s x_r-a_r x_s=0, \end{align*} and the coefficient of $x_s$ is nonzero. If all vectors are zero, the list is already dependent. For the induction step, take a list $(x_1,\ldots,x_m)$ in $k^n$ with $m>n$. Write \begin{align*} x_j=(a_{1j},a_{2j},\ldots,a_{nj}) \end{align*} for each $j$. If every first coordinate is zero, deleting the first coordinate gives a list of $m>n-1$ vectors in $k^{n-1}$. By the induction hypothesis, those projected vectors satisfy a nontrivial linear relation, and since all deleted coordinates were zero, that same relation holds in $k^n$. If some first coordinate is nonzero, reindex so that $a_{11}\neq 0$. For $j=2,\ldots,m$, define \begin{align*} y_j=x_j-\frac{a_{1j}}{a_{11}}x_1. \end{align*} This choice is exactly Gaussian elimination: it kills the first coordinate of each $y_j$, because \begin{align*} a_{1j}-\frac{a_{1j}}{a_{11}}a_{11}=0. \end{align*} After deleting the first coordinate, the list $(\pi(y_2),\ldots,\pi(y_m))$ has $m-1>n-1$ vectors in $k^{n-1}$, so the induction hypothesis gives scalars $c_2,\ldots,c_m$, not all zero, with \begin{align*} \sum_{j=2}^m c_j\pi(y_j)=0. \end{align*} Because each $y_j$ has first coordinate zero, this is equivalent to \begin{align*} \sum_{j=2}^m c_jy_j=0. \end{align*} Substituting the definition of $y_j$ produces the relation \begin{align*} \sum_{j=2}^m c_jx_j-\left(\sum_{j=2}^m c_j\frac{a_{1j}}{a_{11}}\right)x_1=0. \end{align*} At least one coefficient among $x_2,\ldots,x_m$ is nonzero, so the relation is nontrivial. Therefore any list of more than $n$ vectors in $k^n$, and hence in $V$, is linearly dependent.[/guided]

[step:Construct a finite basis of $W$ by a terminating independent-list process] If $W=\{0\}$, then the empty list is a basis of $W$, so $W$ is finite-dimensional and $\dim_k W=0\leq n$. Assume $W\neq\{0\}$. We construct a list in $W$ as follows. Choose $w_1\in W$ with $w_1\neq 0$. Having chosen a linearly independent list $(w_1,\ldots,w_r)$ in $W$, if \begin{align*} W=\operatorname{span}_k\{w_1,\ldots,w_r\}, \end{align*} then stop. If not, choose \begin{align*} w_{r+1}\in W\setminus \operatorname{span}_k\{w_1,\ldots,w_r\}. \end{align*} The enlarged list $(w_1,\ldots,w_r,w_{r+1})$ is linearly independent: if \begin{align*} \sum_{i=1}^{r+1} c_iw_i=0 \end{align*} with $c_i\in k$, then $c_{r+1}\neq 0$ would imply \begin{align*} w_{r+1}=-c_{r+1}^{-1}\sum_{i=1}^r c_iw_i\in \operatorname{span}_k\{w_1,\ldots,w_r\}, \end{align*} contrary to the choice of $w_{r+1}$. Hence $c_{r+1}=0$, and then the [linear independence](/page/Linear%20Independence) of $(w_1,\ldots,w_r)$ gives $c_1=\cdots=c_r=0$. The process cannot produce more than $n$ vectors, because every list in $W$ is also a list in $V$, and the preceding step shows that every linearly independent list in $V$ has length at most $n$. Therefore the construction stops after some integer $r$ with $0\leq r\leq n$. At stopping time, \begin{align*} W=\operatorname{span}_k\{w_1,\ldots,w_r\}, \end{align*} and the list $(w_1,\ldots,w_r)$ is linearly independent. Thus it is a basis of $W$, so $W$ is finite-dimensional and \begin{align*} \dim_k W=r\leq n=\dim_k V. \end{align*} [/step]

[step:Use equality of dimensions to force the subspace to be the whole space] Assume now that $\dim_k W=\dim_k V=n$. Let $(w_1,\ldots,w_n)$ be a basis of $W$, whose existence follows from the preceding step. Since each $w_i$ lies in $W\subset V$, the same list is a linearly independent list in $V$. We prove that $(w_1,\ldots,w_n)$ spans $V$. Suppose not. Then there exists \begin{align*} v\in V\setminus \operatorname{span}_k\{w_1,\ldots,w_n\}. \end{align*} By the same independence argument used in the construction step, the list $(w_1,\ldots,w_n,v)$ is linearly independent in $V$. This list has $n+1$ vectors, contradicting the first step. Hence \begin{align*} V=\operatorname{span}_k\{w_1,\ldots,w_n\}. \end{align*} But also \begin{align*} W=\operatorname{span}_k\{w_1,\ldots,w_n\}. \end{align*} Therefore $W=V$, completing the proof. [/step]