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