Proof of A Finite Spanning Family Contains a Basis

Write (V$k$) for claim $k$ of Elementary Identities in a Vector Space and (O$k$) for claim $k$ of Properties of the Order on the Natural Numbers.

Let $A$ be the set of those $q\in\mathbb{N}$ such that for every $v\in V^{q}$ spanning $V$ there are a natural number $r$ with $r\le q$ and a basis $e\in V^{r}$ of $V$.

Base case. Let $v\in V^{1}$ span $V$. Since $V\ne\{0_{V}\}$ there is $u\in V$ with $u\ne 0_{V}$, and spanning gives $c\in K^{1}$ with $u=\sum_{k=1}^{1}c_{k}v_{k}=c_{1}v_{1}$, the last equality by claim 1 of Properties of Finite Sums of Vectors. Were $v_{1}=0_{V}$, this would give $u=c_{1}0_{V}=0_{V}$ by (V4); hence $v_{1}\ne 0_{V}$.

Now let $c\in K^{1}$ satisfy $\sum_{k=1}^{1}c_{k}v_{k}=0_{V}$, that is, $c_{1}v_{1}=0_{V}$. By (V6) and $v_{1}\ne 0_{V}$ we get $c_{1}=0$, so $v$ is linearly independent. Being also spanning, $v$ is a basis of $V$, so $r=1$ and $e=v$ work and $1\in A$.

Induction step. Let $q\in A$ and let $v\in V^{q+1}$ span $V$. If $v$ is linearly independent, then $v$ is a basis of $V$ and $r=q+1$ works.

Otherwise claim 3 of Elementary Properties of Linear Independence, applied to the tuple $v$ of length $q+1$, yields $j\in[q+1]$ with $v_{j}$ in the span of $v^{(j)}$, where $v^{(j)}\in V^{q}$ is obtained from $v$ by omitting the $j$-th component as in Extraction of a Summand from a Finite Sum of Vectors. By Dropping a Redundant Vector from a Spanning Family, the tuple $v^{(j)}$ spans $V$. Since $q\in A$, there are $r\le q$ and a basis $e\in V^{r}$ of $V$; and $q\le q+1$ by (O6) and (O1), so $r\le q+1$ by (O1). Hence $q+1\in A$.

By Principle of Induction for the Natural Numbers we conclude $A=\mathbb{N}$; in particular $n\in A$, which applied to the given spanning tuple $v$ is the assertion.