$\operatorname{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$, and $\operatorname{span}(\varnothing) = \{0_V\}$

$L(S) \subseteq V$ by construction, and $0_V \in L(S)$: take $n = 0$, whose only lists are the empty ones, and whose sum is the empty sum $0_V$. In particular $L(S)$ is nonempty.

$S \subseteq L(S)$: for $w \in S$ take $n = 1$ with $\lambda_0 = 1_F$ and $v_0 = w$, so that $\sum_{i<1} \lambda_i v_i = 0_V + 1_F w = 1_F w = w$, using the recursion at $\sigma(0) = 1$, the identity law and (V5).

Extending a list. Let $A$ be a set, $n \in \mathbb{N}$, $u : n \to A$ and $x \in A$. Since $\sigma(n) = n \cup \{n\}$ and $n \notin n$, there is exactly one $u' : \sigma(n) \to A$ with $u'(i) = u(i)$ for $i < n$ and $u'(n) = x$; and when $A = V$, the recursion gives $\sum_{i<\sigma(n)} u'_i = \bigl(\sum_{i<n} u_i\bigr) + x$.

Scalars pass through a finite sum: for every $\mu \in F$, every $n \in \mathbb{N}$ and every list $u : n \to V$, $\mu \sum_{i<n} u_i = \sum_{i<n} \mu u_i$. By induction on $n$: at $n = 0$ both sides are $0_V$, since $\mu 0_V = 0_V$; and if the identity holds at $n$, then for a list on $\sigma(n)$ we get $\mu \sum_{i<\sigma(n)} u_i = \mu\bigl(\sum_{i<n} u_i + u_n\bigr) = \mu \sum_{i<n} u_i + \mu u_n = \sum_{i<n} \mu u_i + \mu u_n = \sum_{i<\sigma(n)} \mu u_i$, by (V2), the inductive hypothesis and the recursion.

A linear subspace $W$ with $S \subseteq W$ contains every linear combination of elements of $S$. By induction on $n$: at $n = 0$ the sum is $0_V \in W$ by (W1); and if every such combination of length $n$ lies in $W$, then for lists $\lambda : \sigma(n) \to F$ and $v : \sigma(n) \to S$ we have $\sum_{i<\sigma(n)} \lambda_i v_i = \bigl(\sum_{i<n} \lambda_i v_i\bigr) + \lambda_n v_n$, whose first summand lies in $W$ by the inductive hypothesis and whose second lies in $W$ by (W3) applied to $v_n \in S \subseteq W$, so the whole lies in $W$ by (W2).

The only function $v : n \to \varnothing$ has $n = 0$: if $n \ne 0$ then $0 \in n$, and $v(0)$ would be an element of $\varnothing$. So the only linear combination of elements of $\varnothing$ is the empty sum, and $L(\varnothing) = \{0_V\}$.

$L(S)$ is closed under scalar multiplication: if $w = \sum_{i<n} \lambda_i v_i$ with $\lambda : n \to F$ and $v : n \to S$, and $\mu \in F$, then $\mu w = \sum_{i<n} \mu(\lambda_i v_i) = \sum_{i<n} (\mu\lambda_i) v_i$ by (V4), and $i \mapsto \mu\lambda_i$ is a list $n \to F$, so $\mu w \in L(S)$.

$L(S)$ is closed under addition. Fix $x \in L(S)$; we show by induction on $n$ that $x + \sum_{i<n} \mu_i v_i \in L(S)$ for all lists $\mu : n \to F$ and $v : n \to S$. At $n = 0$ the sum is $0_V$ and $x + 0_V = x \in L(S)$. Assume it at $n$ and let $\mu : \sigma(n) \to F$, $v : \sigma(n) \to S$; then $x + \sum_{i<\sigma(n)} \mu_i v_i = \bigl(x + \sum_{i<n} \mu_i v_i\bigr) + \mu_n v_n$ by the recursion and associativity, and $y := x + \sum_{i<n} \mu_i v_i$ lies in $L(S)$ by the inductive hypothesis, say $y = \sum_{i<m} \nu_i w_i$ with $\nu : m \to F$ and $w : m \to S$; extending $\nu$ by $\mu_n$ and $w$ by $v_n$ as in step 1.3 gives lists on $\sigma(m)$ whose combination is $y + \mu_n v_n$, so $x + \sum_{i<\sigma(n)} \mu_i v_i \in L(S)$.

$L(S) \subseteq \operatorname{span}(S)$: the span is a linear subspace of $V$ containing $S$, so by step 1.5 it contains every linear combination of elements of $S$.

$L(S)$ is a linear subspace of $V$: it is nonempty, and for $\lambda \in F$ and $u, v \in L(S)$ we have $\lambda u \in L(S)$ and then $\lambda u + v \in L(S)$, so the one-step test applies.

$\operatorname{span}(S) \subseteq L(S)$: by steps 1.2 and 3.1 the set $L(S)$ is a linear subspace of $V$ containing $S$, and the span is contained in every such subspace.

Combining the two inclusions, $\operatorname{span}(S) = L(S)$.

Taking $S = \varnothing$ and using step 1.6 gives $\operatorname{span}(\varnothing) = L(\varnothing) = \{0_V\}$; and for arbitrary $S$, the empty combination shows $0_V \in L(S) = \operatorname{span}(S)$.