A finite spanning list contains a basis, without choice

Start with the empty retained list $B_0$. For $1\le j\le n$, append $v_j$ to $B_{j-1}$ if $v_j\mathrm{\notin }\mathrm{span}(B_{j-1})$, and otherwise set $B_j=B_{j-1}$. This finite procedure makes each decision from the current vector and the already constructed span, so it uses no choice.

For every $j$, $\mathrm{span}(B_j)=\mathrm{span}(v_1,\dots ,v_j)$. At $j=0$ both spans are $\{0\}$ by the empty-sum clause of [F1]. If $v_j$ already lies in the previous span, omitting it does not change the span; if it does not, adjoining it gives exactly the span after adding $v_j$ to the original prefix. Induction [F4] proves the claim through $j=n$.

The retained list is linearly independent. If a nontrivial linear relation existed, let $b$ be its last vector with nonzero coefficient $\lambda$. Solving for $b$ using ${\lambda }^{-1}$ from [F3] would put $b$ in the span of the earlier retained vectors, contrary to the rule by which $b$ was appended. The empty retained list is independent by [F2] as well.

By step 2.1 the retained list spans $W$, and by step 2.2 it is linearly independent. It is therefore a basis of $W$ by [F2]; it is finite because it is a sublist of the original finite list. By the definition of finite-dimensionality Finite-dimensional vector space, and its dimension ${\dim }_{F}V$; infinite-dimensional means having no finite basis, $W$ is finite-dimensional.