let V be free finitely-generated Z_Module; :: thesis: V is finite-rank

ex A being finite Subset of V st A is Basis of V by FG02;

hence V is finite-rank by ZMODUL03:def 3; :: thesis: verum

ex A being finite Subset of V st A is Basis of V by FG02;

hence V is finite-rank by ZMODUL03:def 3; :: thesis: verum