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 $|L| = 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 \notin \{c,p\}$ is well defined, the clauses agreeing when $c = p$, and satisfies $\tau \circ \tau = \mathrm{id}$, 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 \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 \notin p$, there is exactly one $f' : \sigma(p) \to A$ with $f'(i) = f(i)$ for $i < p$ and $f'(p) = y$, and $f'$ is injective because $f$ is and $y$ is not a value of $f$.

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

The exchange induction. For every $m \in \mathbb{N}$: if $L' \subseteq V$ is linearly independent with $L' \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 $\operatorname{span}(L' \cup T) = V$. By induction on $m$. At $m = 0$ we have $L' = \varnothing$, since $\varnothing$ is the only set equinumerous with $0$; take $T := S$, note $0 + n = n$ so $k = n$, and $\operatorname{span}(\varnothing \cup S) = \operatorname{span}(S) = V$; and $0 \le n$. Assume the statement at $m$ and let $L''$ be independent with $L'' \approx \sigma(m)$. Then $L'' \ne \varnothing$, so fix $w \in L''$ and put $L' := L'' \setminus \{w\}$, which is independent and, by step 1.1, satisfies $L' \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 $\operatorname{span}(L' \cup T) = V$. Moreover $w \notin \operatorname{span}(L')$: otherwise $w \in \operatorname{span}(L'' \setminus \{w\})$ would make $L''$ dependent. So step 1.3 supplies $t \in T$ with $t \notin L'$ and $\operatorname{span}(L'' \cup (T \setminus \{t\})) = V$, using $L' \cup \{w\} = L''$. Since $t \in T$ we have $k \ne 0$, say $k = \sigma(k')$, and step 1.1 gives $T \setminus \{t\} \approx k'$; finally $\sigma(m) + k' = \sigma(m + k') = m + \sigma(k') = m + k = n$, so $\sigma(m) \le n$ and $k'$ is the unique natural with $\sigma(m) + k' = 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 $\operatorname{span}(L \cup T) = V$; these are claims 1 and 2.