Solution (source code)

= Solution

For the <equal-cardinality basis criterion>, because $S$ <spans> $V$, repeatedly remove a <vector> whenever it is a <linear combination> of the others. Such a removal does not change the <span>. The finite process ends with a <linearly independent> spanning subset $T$, hence a <basis> of $V$.

If the original $S$ were <linearly dependent>, at least one removal would occur and $|T|<n$. But a <basis> of an $n$-dimensional <vector space> has $n$ <vectors>. Equivalently, apply the allowed claim to the <basis> $T$ and any fixed $n$-vector <basis> of $V$: the latter would wrongly be <linearly dependent>. Thus no removal was possible. \b[The original <spanning set> is <linearly independent> and therefore a <basis>.]