Solution (source code)

= Solution

The <Steinitz exchange lemma> says that if $w_1,\ldots,w_m$ span a <vector space> and $v_1,\ldots,v_r$ are <linearly independent>, then $r\le m$, and after reordering the $w_j$, the family $v_1,\ldots,v_r,w_{r+1},\ldots,w_m$ still spans. Here is a proof. Suppose the first $k-1$ replacements have been made. Express $v_k$ in that spanning family. Some coefficient of a remaining $w_j$ must be nonzero, since otherwise $v_k$ belongs to the <span> of $v_1,\ldots,v_{k-1}$, contrary to <linear independence>. Solve for that $w_j$ and replace it by $v_k$; this preserves spanning. If $r>m$, the first $m$ replacements leave a spanning family $v_1,\ldots,v_m$, contradicting <linear independence> of the first $m+1$ vectors. This proves both assertions.

Now suppose $S$ is <linearly independent> and spans $\mathbb R^n$. Express each member of the <standard basis> using finitely many members of $S$, and let $S_0$ be the finite union of those members. Then $S_0$ spans. No element of $S\setminus S_0$ can exist, since it would be a <linear combination> of $S_0$ and violate <linear independence>. Thus $S$ is finite. Applying the <Steinitz exchange lemma> in both directions to $S$ and the <standard basis> gives $|S|\le n$ and $n\le |S|$. Hence $\boxed{|S|=n}$.