Proof of Dropping a Redundant Vector Does Not Change the Span

Routine facts about mutual inclusion and about removing one element from a class are used without comment (Toolkit for AL2). Write $S=\operatorname{span}(v_{1},\dots,v_{n+1})$ and $S^{(j)}=\operatorname{span}(v^{(j)})$; both are linear subspaces of $V$ by The Span of a Finite Family is the Smallest Subspace Containing It (ii). We prove the two inclusions.

Each component $v^{(j)}_{i}=v_{g_{j}(i)}$ of $v^{(j)}$ is a vector of the family $v$ and so lies in $S$ by The Span of a Finite Family is the Smallest Subspace Containing It (ii). Applying The Span of a Finite Family is the Smallest Subspace Containing It (iii) to the family $v^{(j)}$ and the subspace $S$ gives $S^{(j)}\subseteq S$.

Conversely, let $i\in[n+1]$. If $i\neq j$, there is $i'\in[n]$ with $g_{j}(i')=i$, since $g_{j}$ maps $[n]$ onto $[n+1]\setminus\{j\}$ (Bijections between Intervals: the Gap Map and the Reversal (i)); then $v_{i}=v^{(j)}_{i'}$ lies in $S^{(j)}$ by The Span of a Finite Family is the Smallest Subspace Containing It (ii). If $i=j$, then $v_{j}\in S^{(j)}$ by hypothesis. So every vector of $v$ lies in the subspace $S^{(j)}$, and $S\subseteq S^{(j)}$ by The Span of a Finite Family is the Smallest Subspace Containing It (iii).

The two inclusions give $S^{(j)}=S$, which is (i).