theorem :: ZMODUL01:78

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