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'$, and let $\iota : \sigma(m') \to n$ be injective with $u : n \to V$ vanishing off $\iota[\sigma(m')]$. Put $j_0 := \iota(m') < 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'$ be the restriction of $\iota$ to $m'$, which is injective. Then $u^{(j_0)}$ vanishes off $\iota'[m']$: it vanishes at $j_0$ by construction, and a $j \ne j_0$ outside $\iota'[m']$ is outside $\iota[\sigma(m')]$, so $u_j = 0_V$. The inductive hypothesis therefore gives $\sum_{j<n} u^{(j_0)}_j = \sum_{i<m'} u^{(j_0)}_{\iota(i)} = \sum_{i<m'} u_{\iota(i)}$, the second equality because $\iota(i) \ne j_0$ for $i < m'$ by injectivity. Finally (F3) at $j_0$ gives $\sum_{j<n} u_j = u_{j_0} + \sum_{j<n} u^{(j_0)}_j = \sum_{i<m'} u_{\iota(i)} + u_{\iota(m')} = \sum_{i<\sigma(m')} u_{\iota(i)}$, by commutativity and the recursion.

Claim 2, the deletion map. Fix $n' \in \mathbb{N}$ and $k < \sigma(n')$, so $k \le n'$. The two clauses define a function $\delta_k : n' \to \sigma(n')$: for $i < k$ we have $i < k \le n'$, hence $i < \sigma(n')$, and for $k \le i < n'$ we have $\sigma(i) \le n' < \sigma(n')$. 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') \setminus \{k\}$: a $j < \sigma(n')$ with $j < k$ is $\delta_k(j)$; a $j < \sigma(n')$ with $k < j$ is nonzero, hence $j = \sigma(i)$ for some $i$, and then $i < j \le n'$ gives $i < n'$ 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] = \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 = \bigl(\sum_{i<a} c_i\bigr) + \bigl(\sum_{j<q} c_{a+j}\bigr)$, 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 \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 + \bigl(u_k + \sum_{i<n} w_i\bigr)$, 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 \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 \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 \ne j$, and put $u_i := \lambda_i v_i$, so $u_i = 0_F v_i = 0_V$ for every $i \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 \ne 0_F$, contradicting independence. So $v_i \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') \to V$ with $u_k = 0_V$ for some $k < \sigma(n')$. By step 1.2 the map $\delta_k$ is injective with image $\sigma(n') \setminus \{k\}$, so $u$ vanishes off that image, and claim 1, proved in step 1.1, gives $\sum_{j<\sigma(n')} u_j = \sum_{i<n'} 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.