theorem :: ZMODUL01:80

for V being Z_Module
for W1, W2 being strict Submodule of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2 by VECTSP_4:70;