A subset $S \subseteq V$ is linearly dependent if and only if some $s \in S$ lies in $\operatorname{span}(S \setminus \{s\})$; and $\operatorname{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 \notin x[m]$, extend $x$ to $x' : \sigma(m) \to V$ by $x'_m := w_p$ and $\nu$ to $\nu'$ by $\nu'_m := \mu_p$; then $x'$ is injective with $x'[\sigma(m)] \subseteq w[\sigma(p)]$ and the recursion gives $\sum_{i<\sigma(m)}\nu'_i x'_i = \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 := \nu_k + \mu_p$ and $\nu'_i := \nu_i$ for $i \ne k$; applying (F3) at $k$ to the lists $i \mapsto \nu_i x_i$ and $i \mapsto \nu'_i 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 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 $\operatorname{span}(S)$, so the right-hand set is contained in $\operatorname{span}(S)$. Conversely an element of $\operatorname{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 \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^{(j)}_i$, 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^{(j)}_i = \lambda'_i v_i$ where $\lambda'_j := 0_F$ and $\lambda'_i := \lambda_i$ for $i \ne j$, since $0_F v_j = 0_V$; also $n \ne 0$, say $n = \sigma(n')$, and the entry of this list at $j$ is $0_V$, so deleting the index $j$ gives $R = \sum_{i<n'}\lambda'_{\delta_j(i)} v_{\delta_j(i)}$. Applying step 1.2 to the scalar $-\lambda_j^{-1}$ gives $v_j = \sum_{i<n'}\kappa_i y_i$ with $\kappa_i := (-\lambda_j^{-1})\lambda'_{\delta_j(i)}$ 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 $\operatorname{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 \operatorname{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 \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 \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.