Vector space/Finitely generated/Length of every basis/Fact/Proof
Proof
Let and denote two bases of . According to the basis exchange theorem, applied to the basis and the linearly independent family , we obtain . When we apply the theorem with roles reversed, we get , thus .