Solution (source code)

= Solution

If $S$ is <linearly independent> and has $n$ elements, apply the <Steinitz exchange lemma> with $S$ as the independent family and the <standard basis> as the spanning family. All $n$ members of the <standard basis> are replaced, leaving $S$ itself spanning. Thus $\boxed{\operatorname{span}S=\mathbb R^n}$, so $S$ is a <basis>.