theorem :: ZMODUL01:86

for V being Z_Module
for W being Submodule of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W ) by VECTSP_4:76;