Equal-cardinality basis criterion (source code)

= Equal-cardinality basis criterion

Let $V$ have finite <dimension> $n$ and let $S\subseteq V$ have $n$ <vectors>. Then spanning, <linear independence> and being a <basis> are equivalent. From a <spanning set>, remove redundant <vectors> until an independent <spanning set> remains. A removal would give a <basis> of fewer than $n$ <vectors>, contradicting <dimension> invariance. Conversely, if $S$ is independent and a <vector> lies outside its <span>, adjoining it gives $n+1$ independent <vectors>, again impossible. Thus an independent $S$ <spans>.