[proofplan]
We iteratively remove redundant vectors from the spanning set. At each stage, if some vector $w_j$ lies in the span of the remaining vectors, we delete it; the remaining set still spans $V$. We repeat until no vector is redundant, at which point the surviving subset is linearly independent and still spans $V$, hence is a basis.
[/proofplan]
[step:Describe the reduction algorithm and define the sequence of spanning sets]
Define $S_0 := \{w_1, \ldots, w_m\}$. We construct a decreasing sequence of sets $S_0 \supset S_1 \supset \cdots$ as follows. Given $S_i$, check whether there exists some $w_j \in S_i$ such that $w_j \in \operatorname{span}(S_i \setminus \{w_j\})$. If such a $w_j$ exists, set $S_{i+1} := S_i \setminus \{w_j\}$. If no such $w_j$ exists, the algorithm terminates and we set $S^* := S_i$.
Since $|S_{i+1}| = |S_i| - 1$ and $|S_i| \ge 0$, the algorithm terminates after at most $m$ iterations.
[/step]
[step:Verify that each reduction preserves spanning]
We show that $\operatorname{span}(S_{i+1}) = \operatorname{span}(S_i)$ at each reduction step.
Suppose $S_{i+1} = S_i \setminus \{w_j\}$ where $w_j \in \operatorname{span}(S_i \setminus \{w_j\}) = \operatorname{span}(S_{i+1})$. The inclusion $\operatorname{span}(S_{i+1}) \subset \operatorname{span}(S_i)$ is immediate since $S_{i+1} \subset S_i$. For the reverse inclusion, every element of $S_i$ is either in $S_{i+1}$ or is $w_j$, and $w_j \in \operatorname{span}(S_{i+1})$ by the choice of $w_j$. Therefore every element of $S_i$ lies in $\operatorname{span}(S_{i+1})$, which gives $\operatorname{span}(S_i) \subset \operatorname{span}(S_{i+1})$.
By induction on the number of steps, $\operatorname{span}(S^*) = \operatorname{span}(S_0) = V$.
[guided]
We must show $\operatorname{span}(S_{i+1}) = \operatorname{span}(S_i)$, establishing that removing a redundant vector does not shrink the span.
Since $S_{i+1} = S_i \setminus \{w_j\} \subset S_i$, every linear combination of elements of $S_{i+1}$ is also a linear combination of elements of $S_i$. This gives the inclusion $\operatorname{span}(S_{i+1}) \subset \operatorname{span}(S_i)$.
For the reverse inclusion, we need to show that every element of $S_i$ belongs to $\operatorname{span}(S_{i+1})$. The elements of $S_{i+1}$ are trivially in $\operatorname{span}(S_{i+1})$.
The only element of $S_i$ not in $S_{i+1}$ is $w_j$, and by the selection criterion $w_j \in \operatorname{span}(S_i \setminus \{w_j\}) = \operatorname{span}(S_{i+1})$. Therefore every element of $S_i$ lies in $\operatorname{span}(S_{i+1})$, which gives $\operatorname{span}(S_i) \subset \operatorname{span}(S_{i+1})$.
Combining both inclusions yields $\operatorname{span}(S_{i+1}) = \operatorname{span}(S_i)$. Applying this equality inductively across all reduction steps: $\operatorname{span}(S^*) = \operatorname{span}(S_{k-1}) = \cdots = \operatorname{span}(S_0) = V$, so the terminal set $S^*$ still spans $V$.
[/guided]
[/step]
[step:Verify that the terminal set $S^*$ is linearly independent]
The algorithm terminates at $S^*$ precisely when no $w_j \in S^*$ satisfies $w_j \in \operatorname{span}(S^* \setminus \{w_j\})$. We show this implies $S^*$ is linearly independent.
Write $S^* = \{w_{j_1}, \ldots, w_{j_r}\}$. Suppose
\begin{align*}
a_1 w_{j_1} + \cdots + a_r w_{j_r} = 0
\end{align*}
for scalars $a_1, \ldots, a_r$. If some $a_\ell \neq 0$, then
\begin{align*}
w_{j_\ell} = -\frac{a_1}{a_\ell} w_{j_1} - \cdots - \frac{a_{\ell-1}}{a_\ell} w_{j_{\ell-1}} - \frac{a_{\ell+1}}{a_\ell} w_{j_{\ell+1}} - \cdots - \frac{a_r}{a_\ell} w_{j_r},
\end{align*}
so $w_{j_\ell} \in \operatorname{span}(S^* \setminus \{w_{j_\ell}\})$. This contradicts the termination condition. Therefore $a_1 = \cdots = a_r = 0$, and $S^*$ is linearly independent.
[guided]
The contrapositive formulation makes the argument transparent: linear dependence of a finite set is equivalent to one of the vectors being a linear combination of the others.
Concretely, if $S^* = \{w_{j_1}, \ldots, w_{j_r}\}$ is linearly dependent, then there exist scalars $a_1, \ldots, a_r$, not all zero, with
\begin{align*}
a_1 w_{j_1} + \cdots + a_r w_{j_r} = 0.
\end{align*}
Pick any $\ell$ with $a_\ell \neq 0$. Solving for $w_{j_\ell}$:
\begin{align*}
w_{j_\ell} = \sum_{\substack{i=1 \\ i \neq \ell}}^{r} \left(-\frac{a_i}{a_\ell}\right) w_{j_i} \in \operatorname{span}(S^* \setminus \{w_{j_\ell}\}).
\end{align*}
But the algorithm only stops when no element of $S^*$ can be expressed in terms of the others. So $S^*$ being linearly dependent would mean the algorithm should not have terminated -- a contradiction. Therefore $S^*$ is linearly independent.
[/guided]
[/step]
[step:Conclude that $S^*$ is a basis for $V$]
The set $S^*$ spans $V$ (by the second step) and is linearly independent (by the third step). By definition, $S^*$ is a basis for $V$. Since $S^* \subset S_0 = \{w_1, \ldots, w_m\}$, it is a subset of the original spanning set.
[/step]
