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