theorem FG02: :: ZMODUL04:39

for V being free finitely-generated Z_Module ex A being finite Subset of V st A is Basis of V