Vector space/Finitely generated/Basis/Fact/Proof

Proof

Let , , be a finite generating system of , with a finite index set . We argue with the characterization from fact. If the family is minimal, then we have a basis. If not, then there exists some , such that the remaining family where is removed, that is , , is also a generating system. In this case, we can go on with this smaller index set. With this method, we arrive at a subset such that , , is a minimal generating set, hence a basis.