Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never $0_V$, its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent

Claim 1, by induction on $m$. At $m=0$ the image $\iota [0]$ is empty, so $u_j=0_V$ for every $j<n$ and (F1) gives ${\sum }_{j<n}{u}_j=0_V$, which is also the empty sum ${\sum }_{i<0}{u}_{\iota (i)}$. Assume the claim for $m^{\mathrm{\prime }}$, and let $\iota :\sigma (m^{\mathrm{\prime }})\to n$ be injective with $u:n\to V$ vanishing off $\iota [\sigma (m^{\mathrm{\prime }})]$. Put $j_0:=\iota (m^{\mathrm{\prime }})<n$, let $u^{(j_0)}$ be the list agreeing with $u$ off $j_0$ and equal to $0_V$ at $j_0$, and let ${\iota }^{\mathrm{\prime }}$ be the restriction of $\iota$ to $m^{\mathrm{\prime }}$, which is injective. Then $u^{(j_0)}$ vanishes off ${\iota }^{\mathrm{\prime }}[m^{\mathrm{\prime }}]$: it vanishes at $j_0$ by construction, and a $j\mathrm{\ne }{j}_0$ outside ${\iota }^{\mathrm{\prime }}[m^{\mathrm{\prime }}]$ is outside $\iota [\sigma (m^{\mathrm{\prime }})]$, so $u_j=0_V$. The inductive hypothesis therefore gives ${\sum }_{j<n}{u}_j^{(j_0)}={\sum }_{i<m^{\mathrm{\prime }}}{u}_{\iota (i)}^{(j_0)}={\sum }_{i<m^{\mathrm{\prime }}}{u}_{\iota (i)}$, the second equality because $\iota (i)\mathrm{\ne }{j}_0$ for $i<m^{\mathrm{\prime }}$ by injectivity. Finally (F3) at $j_0$ gives ${\sum }_{j<n}{u}_j=u_{j_0}+{\sum }_{j<n}{u}_j^{(j_0)}={\sum }_{i<m^{\mathrm{\prime }}}{u}_{\iota (i)}+u_{\iota (m^{\mathrm{\prime }})}={\sum }_{i<\sigma (m^{\mathrm{\prime }})}{u}_{\iota (i)}$, by commutativity and the recursion.

Claim 2, the deletion map. Fix $n^{\mathrm{\prime }}\in \mathbb{N}$ and $k<\sigma (n^{\mathrm{\prime }})$, so $k\le n^{\mathrm{\prime }}$. The two clauses define a function ${\delta }_k:n^{\mathrm{\prime }}\to \sigma (n^{\mathrm{\prime }})$: for $i<k$ we have $i<k\le n^{\mathrm{\prime }}$, hence $i<\sigma (n^{\mathrm{\prime }})$, and for $k\le i<n^{\mathrm{\prime }}$ we have $\sigma (i)\le n^{\mathrm{\prime }}<\sigma (n^{\mathrm{\prime }})$. It is injective, being injective on each of the two blocks while its values on the first are below $k$ and its values on the second satisfy $k<\sigma (i)$. Its image is $\sigma (n^{\mathrm{\prime }})\setminus \{k\}$: a $j<\sigma (n^{\mathrm{\prime }})$ with $j<k$ is ${\delta }_k(j)$; a $j<\sigma (n^{\mathrm{\prime }})$ with $k<j$ is nonzero, hence $j=\sigma (i)$ for some $i$, and then $i<j\le n^{\mathrm{\prime }}$ gives $i<n^{\mathrm{\prime }}$ while $k<\sigma (i)$ gives $k\le i$, so $j={\delta }_k(i)$; and $k$ itself is not a value, the first block giving values below $k$ and the second values above $k$.

Claim 3, the concatenated list. Let $a,q\in \mathbb{N}$, $y:a\to V$ and $z:q\to V$. Every $i<a+q$ satisfies exactly one of $i<a$ and $a\le i$; in the second case there is $j$ with $a+j=i$, and $a+j<a+q$ forces $j<q$, while $j$ is unique by cancellation of addition. So the clauses $c_i:=y_i$ for $i<a$ and $c_{a+j}:=z_j$ for $j<q$ determine exactly one function $c:a+q\to V$. If $y$ and $z$ are injective with $y[a]\cap z[q]=\mathrm{\varnothing }$, then $c$ is injective: it is injective on each block, and a value from the first block lies in $y[a]$ while a value from the second lies in $z[q]$, two disjoint sets. Its image is $y[a]\cup z[q]$ by the two clauses.

Claim 3, the sum identity. The splitting law for finite sums gives ${\sum }_{i<a+q}{c}_i=\left({\sum }_{i<a}{c}_i\right)+\left({\sum }_{j<q}{c}_{a+j}\right)$, and by the defining clauses $c_i=y_i$ for $i<a$ and $c_{a+j}=z_j$ for $j<q$, so ${\sum }_{i<a+q}{c}_i={\sum }_{i<a}{y}_i+{\sum }_{j<q}{z}_j$.

Claim 4, injectivity. Let $v:n\to V$ be independent and suppose $v_j=v_k$ with $j\mathrm{\ne }k$ and $j,k<n$. Define $\lambda :n\to F$ by ${\lambda }_j=1_F$, ${\lambda }_k=-1_F$ and ${\lambda }_i=0_F$ otherwise, and put $u_i:={\lambda }_i{v}_i$. Extracting the term at $j$ by (F3) and then the term at $k$ from the resulting list gives ${\sum }_{i<n}{u}_i=u_j+(u_k+{\sum }_{i<n}{w}_i)$, where $w$ agrees with $u$ off $\{j,k\}$ and is $0_V$ at both. Every entry of $w$ is $0_V$, since $u_i=0_F{v}_i=0_V$ for $i\mathrm{\notin }\{j,k\}$, so (F1) makes the last sum $0_V$. Hence ${\sum }_{i<n}{\lambda }_i{v}_i=1_F{v}_j+(-1_F)v_k=v_j+(-v_k)=0_V$, while ${\lambda }_j=1_F\mathrm{\ne }{0}_F$, contradicting independence. So $v$ is injective.

Claim 4, no entry equal to $0_V$. Let $v:n\to V$ be independent and suppose $v_j=0_V$ for some $j<n$. Define $\lambda :n\to F$ by ${\lambda }_j=1_F$ and ${\lambda }_i=0_F$ for $i\mathrm{\ne }j$, and put $u_i:={\lambda }_i{v}_i$, so $u_i=0_F{v}_i=0_V$ for every $i\mathrm{\ne }j$. Then (F3) at $j$ together with (F1) gives ${\sum }_{i<n}{\lambda }_i{v}_i=u_j+0_V=1_F{v}_j=v_j=0_V$, while ${\lambda }_j=1_F\mathrm{\ne }{0}_F$, contradicting independence. So $v_i\mathrm{\ne }{0}_V$ for every $i<n$.

Zero extension of a list of scalars. Let $\iota :m\to n$ be injective, let $\mu :m\to F$ and let $v:n\to V$. Because $\iota$ is injective there is exactly one $\lambda :n\to F$ with ${\lambda }_{\iota (i)}={\mu }_i$ for every $i<m$ and ${\lambda }_j=0_F$ for every $j<n$ outside $\iota [m]$. The list $u_j:={\lambda }_j{v}_j$ then satisfies $u_j=0_F{v}_j=0_V$ for every $j$ outside $\iota [m]$, and $u_{\iota (i)}={\mu }_i{v}_{\iota (i)}$ for every $i<m$.

Claim 7. Let $S\subseteq V$ be independent and let $T\subseteq S$. Every injective finite list $w:p\to T$ is in particular an injective finite list into $S$, hence independent; so every injective finite list into $T$ is independent, which is exactly independence of $T$.

Claim 6, from right to left. Suppose $v:n\to V$ is injective and $v[n]$ is an independent subset of $V$. Read as a function $n\to v[n]$, the list $v$ is an injective finite list into $v[n]$, hence independent; the vanishing condition is a condition on sums computed in $V$ and is unaffected by which codomain $v$ is read into, so the list $v:n\to V$ is independent. Moreover $v$ is a bijection $n\to v[n]$, so $v[n]\approx n$.

Claim 2, the consequence. Let $u:\sigma (n^{\mathrm{\prime }})\to V$ with $u_k=0_V$ for some $k<\sigma (n^{\mathrm{\prime }})$. By step 1.2 the map ${\delta }_k$ is injective with image $\sigma (n^{\mathrm{\prime }})\setminus \{k\}$, so $u$ vanishes off that image, and claim 1, proved in step 1.1, gives ${\sum }_{j<\sigma (n^{\mathrm{\prime }})}{u}_j={\sum }_{i<n^{\mathrm{\prime }}}{u}_{{\delta }_k(i)}$.

Claim 5. Let $v:n\to V$ be independent, $\iota :m\to n$ injective, and $\mu :m\to F$ with ${\sum }_{i<m}{\mu }_i{v}_{\iota (i)}=0_V$. Take the zero extension $\lambda$ of step 1.7, so the list $u_j:={\lambda }_j{v}_j$ vanishes off $\iota [m]$ and $u_{\iota (i)}={\mu }_i{v}_{\iota (i)}$. Then step 1.1 gives ${\sum }_{j<n}{\lambda }_j{v}_j={\sum }_{j<n}{u}_j={\sum }_{i<m}{u}_{\iota (i)}={\sum }_{i<m}{\mu }_i{v}_{\iota (i)}=0_V$, so independence of $v$ forces ${\lambda }_j=0_F$ for every $j<n$, and in particular ${\mu }_i={\lambda }_{\iota (i)}=0_F$ for every $i<m$. Hence $v\circ \iota$ is independent.

Claim 6, from left to right. Let $v:n\to V$ be independent; it is injective by step 1.5, so it is a bijection $n\to v[n]$ and has a two-sided inverse there. Let $w:p\to v[n]$ be an injective finite list; then $\iota :=v^{-1}\circ w:p\to n$ is injective and $v\circ \iota =w$, so $w$ is independent by step 2.2. Hence every injective finite list into $v[n]$ is independent, that is, $v[n]$ is an independent subset of $V$, and $v[n]\approx n$.

Claim 1 is step 1.1; claim 2 is step 1.2 with step 2.1; claim 3 is step 1.3 with step 1.4; claim 4 is step 1.5 with step 1.6; claim 5 is step 2.2; claim 6 is step 1.9 with step 3.1; and claim 7 is step 1.8.