The Steinitz exchange lemma: if $L\subseteq V$ is linearly independent and $S\subseteq V$ spans $V$ with $S$ finite of size $n$, then $L$ is finite with $\mathrm{\mid }L\mathrm{\mid }=m\le n$, and there is $T\subseteq S$ of size $n-m$ such that $L\cup T$ spans $V$

Removing one element from a finite set. Let $X\approx \sigma (p)$ and $x\in X$; then $X\setminus \{x\}\approx p$. Take a bijection $g:\sigma (p)\to X$ and let $c$ be the unique index with $g(c)=x$. The map $\tau :\sigma (p)\to \sigma (p)$ with $\tau (c)=p$, $\tau (p)=c$ and $\tau (i)=i$ for $i\mathrm{\notin }\{c,p\}$ is well defined, the clauses agreeing when $c=p$, and satisfies $\tau \circ \tau =\mathrm{i}\mathrm{d}$, so it is a bijection. Then $h:=g\circ \tau$ is a bijection $\sigma (p)\to X$ with $h(p)=x$, and its restriction to $p$ is a bijection onto $X\setminus \{x\}$: it is injective; its values differ from $x$, since $h$ is injective and $h(p)=x$; and every $y\in X\setminus \{x\}$ is $h(i)$ for some $i\in \sigma (p)$ with $i\mathrm{\ne }p$, that is $i<p$.

Extending an injective list by one value. Let $A$ be a set, $f:p\to A$ injective and $y\in A\setminus f[p]$. Since $\sigma (p)=p\cup \{p\}$ and $p\mathrm{\notin }p$, there is exactly one $f^{\mathrm{\prime }}:\sigma (p)\to A$ with $f^{\mathrm{\prime }}(i)=f(i)$ for $i<p$ and $f^{\mathrm{\prime }}(p)=y$, and $f^{\mathrm{\prime }}$ is injective because $f$ is and $y$ is not a value of $f$.

The exchange step. Let $L^{\mathrm{\prime }}\subseteq V$ be linearly independent, $T\subseteq S$, $\mathrm{span}(L^{\mathrm{\prime }}\cup T)=V$, and $w\in V$ with $w\mathrm{\notin }\mathrm{span}(L^{\mathrm{\prime }})$. Then there is $t\in T$ with $t\mathrm{\notin }{L}^{\mathrm{\prime }}$ and $\mathrm{span}((L^{\mathrm{\prime }}\cup \{w\})\cup (T\setminus \{t\}))=V$. Indeed $w\in \mathrm{span}(L^{\mathrm{\prime }}\cup T)$, so $w={\sum }_{i<p}{\nu }_i{x}_i$ for some injective $x:p\to L^{\mathrm{\prime }}\cup T$ and $\nu :p\to F$. Some $i_0<p$ has $x_{i_0}\mathrm{\notin }{L}^{\mathrm{\prime }}$ and ${\nu }_{i_0}\mathrm{\ne }{0}_F$: otherwise ${\nu }_i=0_F$ whenever $x_i\mathrm{\notin }{L}^{\mathrm{\prime }}$, and then, if $L^{\mathrm{\prime }}=\mathrm{\varnothing }$, every term ${\nu }_i{x}_i$ is $0_F{x}_i=0_V$ and (F1) gives $w=0_V\in \mathrm{span}(L^{\mathrm{\prime }})$, while if $L^{\mathrm{\prime }}\mathrm{\ne }\mathrm{\varnothing }$ we may fix $a\in L^{\mathrm{\prime }}$ and put $x_i^{\mathrm{\prime }}:=x_i$ when $x_i\in L^{\mathrm{\prime }}$ and $x_i^{\mathrm{\prime }}:=a$ otherwise, so that ${\nu }_i{x}_i^{\mathrm{\prime }}={\nu }_i{x}_i$ for every $i$, both being $0_V$ in the second case, and $w={\sum }_{i<p}{\nu }_i{x}_i^{\mathrm{\prime }}\in \mathrm{span}(L^{\mathrm{\prime }})$; either way $w\in \mathrm{span}(L^{\mathrm{\prime }})$, contrary to hypothesis. Put $t:=x_{i_0}$, which lies in $T$ and not in $L^{\mathrm{\prime }}$, and put $U:=(L^{\mathrm{\prime }}\cup \{w\})\cup (T\setminus \{t\})$; since $t\mathrm{\notin }{L}^{\mathrm{\prime }}$ we have $(L^{\mathrm{\prime }}\cup T)\setminus \{t\}=L^{\mathrm{\prime }}\cup (T\setminus \{t\})\subseteq U$. Now (F3) at $i_0$ gives $w={\nu }_{i_0}t+R$ with $R={\sum }_{i<p}{\nu }_i^{\mathrm{\prime }}{x}_i$, where ${\nu }_{i_0}^{\mathrm{\prime }}:=0_F$ and ${\nu }_i^{\mathrm{\prime }}:={\nu }_i$ otherwise; the list $i\mapsto {\nu }_i^{\mathrm{\prime }}{x}_i$ has the value $0_V$ at $i_0$, so deleting that index expresses $R$ as a linear combination of the $x_i$ with $i\mathrm{\ne }{i}_0$, all of which lie in $(L^{\mathrm{\prime }}\cup T)\setminus \{t\}$, whence $R\in \mathrm{span}(U)$. Since $w\in U\subseteq \mathrm{span}(U)$ and $\mathrm{span}(U)$ is a linear subspace, ${\nu }_{i_0}t=w+(-R)\in \mathrm{span}(U)$ and therefore $t={\nu }_{i_0}^{-1}({\nu }_{i_0}t)\in \mathrm{span}(U)$. Hence $\mathrm{span}(U)$ contains $L^{\mathrm{\prime }}\cup (T\setminus \{t\})$ together with $t$, that is all of $L^{\mathrm{\prime }}\cup T$, so it contains $\mathrm{span}(L^{\mathrm{\prime }}\cup T)=V$ by minimality of the span.

The exchange induction. For every $m\in \mathbb{N}$: if $L^{\mathrm{\prime }}\subseteq V$ is linearly independent with $L^{\mathrm{\prime }}\approx m$, then $m\le n$ and there is $T\subseteq S$ with $T\approx k$, where $k$ is the unique natural with $m+k=n$, and $\mathrm{span}(L^{\mathrm{\prime }}\cup T)=V$. By induction on $m$. At $m=0$ we have $L^{\mathrm{\prime }}=\mathrm{\varnothing }$, since $\mathrm{\varnothing }$ is the only set equinumerous with $0$; take $T:=S$, note $0+n=n$ so $k=n$, and $\mathrm{span}(\mathrm{\varnothing }\cup S)=\mathrm{span}(S)=V$; and $0\le n$. Assume the statement at $m$ and let $L^{\mathrm{\prime }\mathrm{\prime }}$ be independent with $L^{\mathrm{\prime }\mathrm{\prime }}\approx \sigma (m)$. Then $L^{\mathrm{\prime }\mathrm{\prime }}\mathrm{\ne }\mathrm{\varnothing }$, so fix $w\in L^{\mathrm{\prime }\mathrm{\prime }}$ and put $L^{\mathrm{\prime }}:=L^{\mathrm{\prime }\mathrm{\prime }}\setminus \{w\}$, which is independent and, by step 1.1, satisfies $L^{\mathrm{\prime }}\approx m$. The inductive hypothesis gives $m\le n$, the unique $k$ with $m+k=n$, and $T\subseteq S$ with $T\approx k$ and $\mathrm{span}(L^{\mathrm{\prime }}\cup T)=V$. Moreover $w\mathrm{\notin }\mathrm{span}(L^{\mathrm{\prime }})$: otherwise $w\in \mathrm{span}(L^{\mathrm{\prime }\mathrm{\prime }}\setminus \{w\})$ would make $L^{\mathrm{\prime }\mathrm{\prime }}$ dependent. So step 1.3 supplies $t\in T$ with $t\mathrm{\notin }{L}^{\mathrm{\prime }}$ and $\mathrm{span}(L^{\mathrm{\prime }\mathrm{\prime }}\cup (T\setminus \{t\}))=V$, using $L^{\mathrm{\prime }}\cup \{w\}=L^{\mathrm{\prime }\mathrm{\prime }}$. Since $t\in T$ we have $k\mathrm{\ne }0$, say $k=\sigma (k^{\mathrm{\prime }})$, and step 1.1 gives $T\setminus \{t\}\approx k^{\mathrm{\prime }}$; finally $\sigma (m)+k^{\mathrm{\prime }}=\sigma (m+k^{\mathrm{\prime }})=m+\sigma (k^{\mathrm{\prime }})=m+k=n$, so $\sigma (m)\le n$ and $k^{\mathrm{\prime }}$ is the unique natural with $\sigma (m)+k^{\mathrm{\prime }}=n$. Taking $T\setminus \{t\}\subseteq S$ completes the inductive step.

$L$ is finite. Suppose not. Then for every $p\in \mathbb{N}$ there is an injection $p\to L$: at $p=0$ the empty function serves, and given an injective $f:p\to L$, the image $f[p]$ cannot be all of $L$, since $L\approx p$ would make $L$ finite, so some $y\in L\setminus f[p]$ exists and step 1.2 extends $f$ to an injection $\sigma (p)\to L$. Take $p:=\sigma (n)$ and an injection $f:\sigma (n)\to L$; its image $f[\sigma (n)]$ is a subset of $L$, hence independent, and $f[\sigma (n)]\approx \sigma (n)$. Step 2.1 applied to it gives $\sigma (n)\le n$, while $n<\sigma (n)$, so $n<n$, which is impossible. Hence $L$ is finite.

By step 3.1 the set $L$ is finite, so there is exactly one $m\in \mathbb{N}$ with $L\approx m$, and step 2.1 applied to $L$ gives $m\le n$ together with $T\subseteq S$ satisfying $T\approx k$ for the unique $k$ with $m+k=n$ and $\mathrm{span}(L\cup T)=V$; these are claims 1 and 2.