$\mathrm{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$, and $\mathrm{span}(\mathrm{\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\mathrm{\notin }n$, there is exactly one $u^{\mathrm{\prime }}:\sigma (n)\to A$ with $u^{\mathrm{\prime }}(i)=u(i)$ for $i<n$ and $u^{\mathrm{\prime }}(n)=x$; and when $A=V$, the recursion gives ${\sum }_{i<\sigma (n)}{u}_i^{\mathrm{\prime }}=\left({\sum }_{i<n}{u}_i\right)+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 ({\sum }_{i<n}{u}_i+u_n)=\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=\left({\sum }_{i<n}{\lambda }_i{v}_i\right)+{\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 \mathrm{\varnothing }$ has $n=0$: if $n\mathrm{\ne }0$ then $0\in n$, and $v(0)$ would be an element of $\mathrm{\varnothing }$. So the only linear combination of elements of $\mathrm{\varnothing }$ is the empty sum, and $L(\mathrm{\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=(x+{\sum }_{i<n}{\mu }_i{v}_i)+{\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 \mathrm{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.

$\mathrm{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, $\mathrm{span}(S)=L(S)$.

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