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 (2). 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.