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 .