theorem :: ZMODUL01:77

for R being Ring
for V being LeftMod of R
for v being Vector of V
for W1, W2 being strict Submodule of V st v + W1 = v + W2 holds
W1 = W2 by VECTSP_4:66;