Proof of Dropping a Redundant Vector from a Spanning Family

Let $u\in V$. Since $v$ spans $V$, there is a tuple $c$ of scalars in $K^{n+1}$ with

the finite sum in $V$. Apply Extraction of a Summand from a Finite Sum of Vectors to the tuple $b$ in $V^{n+1}$ with components $b_{k}=c_{k}v_{k}$ and to the index $j$:

Let $c^{(j)}$ be the tuple in $K^{n}$ obtained from $c$ by the same recipe by which $v^{(j)}$ is obtained from $v$, that is, $c^{(j)}_{k}=c_{k}$ for $k<j$ and $c^{(j)}_{k}=c_{k+1}$ for $j\le k$, where $k$ ranges over the natural numbers with $1\le k\le n$. Comparing the two cases of the definition, $b^{(j)}_{k}=c^{(j)}_{k}v^{(j)}_{k}$ for every such $k$, so

By hypothesis $v_{j}$ lies in the span of $v^{(j)}$, so there is a tuple $d$ in $K^{n}$ with $v_{j}=\sum_{k=1}^{n}d_{k}v^{(j)}_{k}$. By claim 3 of Properties of Finite Sums of Vectors and the axiom $\lambda(\mu x)=(\lambda\mu)x$ of Vector Space over a Field,

Hence, by claim 2 of Properties of Finite Sums of Vectors and the distributivity axiom of Vector Space over a Field,

Thus every $u\in V$ has the form $\sum_{k=1}^{n}e_{k}v^{(j)}_{k}$ for a tuple $e$ in $K^{n}$, which is what it means for $v^{(j)}$ to span $V$.