Lemme d'échange de Steinitz

Montrons par récurrence sur $k \leqslant m$ que $k \leqslant n$ et que, quitte à renuméroter les $g_j$, la famille $(f_1, \dots, f_k, g_{k+1}, \dots, g_n)$ engendre $E$. Pour $k = 0$, c'est l'hypothèse.

Supposons le résultat vrai pour $k < m$. Écrivons $$f_{k+1} = \sum_{i \leqslant k} a_i f_i + \sum_{j > k} b_j g_j.$$ Si tous les $b_j$ étaient nuls, en particulier s'il n'y avait aucun $g_j$ d'indice $j > k$, on aurait une relation de dépendance entre $f_1, \dots, f_{k+1}$, ce qui contredit la liberté.

Il existe donc $j > k$, d'où $k + 1 \leqslant n$, avec $b_j \neq 0$ ; on renumérote pour que $j = k + 1$. Alors $$\begin{aligned} g_{k+1} = b_{k+1}^{-1}\Big(f_{k+1} &- \sum_{i \leqslant k} a_i f_i \\ &- \sum_{j > k+1} b_j g_j\Big) \end{aligned}$$ appartient au sous-espace engendré par $(f_1, \dots, f_{k+1}, g_{k+2}, \dots, g_n)$, qui contient donc tous les vecteurs de la famille génératrice précédente : il est égal à $E$.

Pour $k = m$, on obtient $m \leqslant n$.