A subset $S\subseteq V$ is linearly dependent if and only if some $s\in S$ lies in $\mathrm{span}(S\setminus \{s\})$; and $\mathrm{span}(S)$ is already the set of linear combinations of INJECTIVE finite lists into $S$

Collecting repeated entries. For every $p\in \mathbb{N}$, every $w:p\to V$ and every $\mu :p\to F$ there are $m\in \mathbb{N}$, an injective $x:m\to V$ with $x[m]\subseteq w[p]$, and $\nu :m\to F$, with ${\sum }_{i<p}{\mu }_i{w}_i={\sum }_{i<m}{\nu }_i{x}_i$. By induction on $p$: at $p=0$ take $m=0$, both sums being $0_V$. Assume it at $p$, and let $w:\sigma (p)\to V$ and $\mu :\sigma (p)\to F$; applying the hypothesis to the restrictions gives ${\sum }_{i<p}{\mu }_i{w}_i={\sum }_{i<m}{\nu }_i{x}_i$ with $x$ injective and $x[m]\subseteq w[p]$, and the recursion gives ${\sum }_{i<\sigma (p)}{\mu }_i{w}_i={\sum }_{i<m}{\nu }_i{x}_i+{\mu }_p{w}_p$. If $w_p\mathrm{\notin }x[m]$, extend $x$ to $x^{\mathrm{\prime }}:\sigma (m)\to V$ by $x_m^{\mathrm{\prime }}:=w_p$ and $\nu$ to ${\nu }^{\mathrm{\prime }}$ by ${\nu }_m^{\mathrm{\prime }}:={\mu }_p$; then $x^{\mathrm{\prime }}$ is injective with $x^{\mathrm{\prime }}[\sigma (m)]\subseteq w[\sigma (p)]$ and the recursion gives ${\sum }_{i<\sigma (m)}{\nu }_i^{\mathrm{\prime }}{x}_i^{\mathrm{\prime }}={\sum }_{i<m}{\nu }_i{x}_i+{\mu }_p{w}_p$. If instead $w_p=x_k$ for the unique such $k<m$, put ${\nu }_k^{\mathrm{\prime }}:={\nu }_k+{\mu }_p$ and ${\nu }_i^{\mathrm{\prime }}:={\nu }_i$ for $i\mathrm{\ne }k$; applying (F3) at $k$ to the lists $i\mapsto {\nu }_i{x}_i$ and $i\mapsto {\nu }_i^{\mathrm{\prime }}{x}_i$, whose $k$-deleted forms coincide, and using (V3) in the form $({\nu }_k+{\mu }_p)x_k={\nu }_k{x}_k+{\mu }_p{x}_k$, gives ${\sum }_{i<m}{\nu }_i^{\mathrm{\prime }}{x}_i={\sum }_{i<m}{\nu }_i{x}_i+{\mu }_p{x}_k$, which is the required value.

A scalar passes through a finite sum: for $\lambda \in F$, $p\in \mathbb{N}$ and $u:p\to V$, applying (F2) with the all-$0_V$ second list and using (F1) and the identity law gives $\lambda {\sum }_{i<p}{u}_i={\sum }_{i<p}\lambda u_i$; combined with (V4) this yields $\lambda {\sum }_{i<p}{\lambda }_i{v}_i={\sum }_{i<p}(\lambda {\lambda }_i)v_i$ for scalars ${\lambda }_i$ and vectors $v_i$.

Claim 2. Every ${\sum }_{i<m}{\nu }_i{x}_i$ with $x:m\to S$ is a linear combination of elements of $S$, hence lies in $\mathrm{span}(S)$, so the right-hand set is contained in $\mathrm{span}(S)$. Conversely an element of $\mathrm{span}(S)$ is ${\sum }_{i<p}{\mu }_i{w}_i$ for some $w:p\to S$, and step 1.1 rewrites it as ${\sum }_{i<m}{\nu }_i{x}_i$ with $x$ injective and $x[m]\subseteq w[p]\subseteq S$, so $x:m\to S$ is an injective finite list.

Claim 1, from left to right. Let $S$ be dependent, witnessed by an injective $v:n\to S$ and $\lambda :n\to F$ with ${\sum }_{i<n}{\lambda }_i{v}_i=0_V$ and ${\lambda }_j\mathrm{\ne }{0}_F$ for some $j<n$. Put $u_i:={\lambda }_i{v}_i$, so (F3) at $j$ gives $0_V=u_j+R$ with $R:={\sum }_{i<n}{u}_i^{(j)}$, whence $u_j=-R$ and $v_j=1_F{v}_j=({\lambda }_j^{-1}{\lambda }_j)v_j={\lambda }_j^{-1}({\lambda }_j{v}_j)={\lambda }_j^{-1}(-R)=(-{\lambda }_j^{-1})R$. Now $u_i^{(j)}={\lambda }_i^{\mathrm{\prime }}{v}_i$ where ${\lambda }_j^{\mathrm{\prime }}:=0_F$ and ${\lambda }_i^{\mathrm{\prime }}:={\lambda }_i$ for $i\mathrm{\ne }j$, since $0_F{v}_j=0_V$; also $n\mathrm{\ne }0$, say $n=\sigma (n^{\mathrm{\prime }})$, and the entry of this list at $j$ is $0_V$, so deleting the index $j$ gives $R={\sum }_{i<n^{\mathrm{\prime }}}{\lambda }_{{\delta }_j(i)}^{\mathrm{\prime }}{v}_{{\delta }_j(i)}$. Applying step 1.2 to the scalar $-{\lambda }_j^{-1}$ gives $v_j={\sum }_{i<n^{\mathrm{\prime }}}{\kappa }_i{y}_i$ with ${\kappa }_i:=(-{\lambda }_j^{-1}){\lambda }_{{\delta }_j(i)}^{\mathrm{\prime }}$ and $y:=v\circ {\delta }_j$. Since ${\delta }_j$ has image $n\setminus \{j\}$ and $v$ is injective, $y$ takes its values in $S\setminus \{v_j\}$, so $v_j$ is a linear combination of elements of $S\setminus \{v_j\}$ and therefore lies in $\mathrm{span}(S\setminus \{v_j\})$. Taking $s:=v_j\in S$ finishes this direction.

Claim 1, from right to left. Let $s\in S$ with $s\in \mathrm{span}(S\setminus \{s\})$. By step 2.1 applied to $S\setminus \{s\}$ there are $m$, an injective $x:m\to S\setminus \{s\}$ and $\nu :m\to F$ with $s={\sum }_{i<m}{\nu }_i{x}_i$. Extend $x$ to $v:\sigma (m)\to S$ by $v_m:=s$, which is injective because $s\mathrm{\notin }x[m]$, and extend $\nu$ to $\lambda :\sigma (m)\to F$ by ${\lambda }_m:=-1_F$. The recursion then gives ${\sum }_{i<\sigma (m)}{\lambda }_i{v}_i={\sum }_{i<m}{\nu }_i{x}_i+(-1_F)s=s+(-s)=0_V$, while ${\lambda }_m=-1_F\mathrm{\ne }{0}_F$, since $-1_F=0_F$ would give $1_F=0_F$. So $v$ is an injective finite list into $S$ that is dependent, and $S$ is dependent.

Claim 1 is steps 2.2 and 3.1 together, and claim 2 is step 2.1.