Solution (source code)

= Solution

Expand $e_{r+1}$ in the given <spanning set>:
$$
e_{r+1}=\sum_{i=1}^ra_ie_i+\sum_{j=r+1}^mb_jf_j.
$$
Some $b_j$ must be nonzero, since otherwise $e_{r+1}$ would lie in the span of the earlier $e_i$, contradicting <linear independence>. Reorder the remaining $f_j$ so $b_{r+1}\ne0$. Solving this equation for $f_{r+1}$ expresses it in terms of $e_1,\ldots,e_{r+1},f_{r+2},\ldots,f_m$. Every member of the old <spanning set> is therefore in the new span, so \b[the replacement set still spans $V$]. This proves the needed step of the <Steinitz exchange lemma> directly.

Starting with $f_1,\ldots,f_m$, apply that replacement successively to $e_1,e_2,\ldots$. After $r\leq m$ steps the spanning list is $e_1,\ldots,e_r$ together with $m-r$ unreplaced $f$'s. If $n>m$, after $m$ replacements the list $e_1,\ldots,e_m$ spans $V$, forcing $e_{m+1}$ to be a <linear combination> of it. That contradicts <linear independence>. Hence \b[$\boxed{n\leq m}$].