theorem :: ZMODUL01:84

for V being Z_Module holds the carrier of V is Coset of (Omega). V by VECTSP_4:74;