theorem :: ZMODUL01:81

for V being Z_Module
for v being Vector of V holds {v} is Coset of (0). V by VECTSP_4:71;