:: deftheorem defines finitely-generated ZMODUL03:def 4 :
for V being Z_Module holds
( V is finitely-generated iff ex A being finite Subset of V st Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) );