A Finite Spanning Family Contains a Basis

Let $K$ be a \reftext{def:field-c54-2026b}{field}, let $V$ be a \reftext{def:vector-space-2026a}{vector space over $K$} with \reftext{lem:vector-space-basic-identities-2026a}{zero vector} $0_{V}$, and suppose $V\ne\{0_{V}\}$. Let $n$ be a \reftext{def:natural-numbers-2026a}{natural number} and let $v\in V^{n}$ be an \reftext{def:finite-tuple-power-2026a}{$n$-tuple} in $V$ that \reftext{def:spanning-finite-family-2026a}{spans} $V$.

Then there are a natural number $r$ with $r\le n$, in the \reftext{def:order-natural-numbers-2026a}{order} on $\mathbb{N}$, and a tuple $e\in V^{r}$ that is a \reftext{def:finite-basis-2026a}{basis} of $V$.