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