Dimension d'un sous-espace : énoncé (MPSI)

Posons $n = \dim E$. Une famille libre de $F$ est libre dans $E$, donc a au plus $n$ vecteurs. On peut donc choisir une famille libre $(f_1, \dots, f_p)$ de $F$ de cardinal $p$ maximal, avec $p \leq n$. Pour $x \in F$, la famille $(f_1, \dots, f_p, x)$ est liée par maximalité, donc $x \in \operatorname{Vect}(f_1, \dots, f_p)$ (contraposée de la propriété d'ajout d'un vecteur). Ainsi $(f_1, \dots, f_p)$ est une base de $F$ : $F$ est de dimension finie et $\dim F = p \leq n$.

Si $\dim F = n$, une base de $F$ est une famille libre de $E$ à $n$ vecteurs, donc une base de $E$ ; elle engendre $E$, d'où $E \subset F$, puis $F = E$. La réciproque est évidente.