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

consider A being finite Subset of V such that

A1: A is Basis of V by ZMODUL03:def 3;

take A ; :: according to ZMODUL03:def 4 :: thesis: Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

thus Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A1, VECTSP_7:def 3; :: thesis: verum

consider A being finite Subset of V such that

A1: A is Basis of V by ZMODUL03:def 3;

take A ; :: according to ZMODUL03:def 4 :: thesis: Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

thus Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A1, VECTSP_7:def 3; :: thesis: verum