1. Énoncé : extraire une base d'une famille génératrice. 2. Compléter une famille libre en base. 3. Démonstration par échange de Steinitz. 4. Conséquence : dimension d'un espace de dimension finie
Lemme d'échange. Existence de complémentaires