theorem Th64: :: RMOD_2:64
for R being Ring
for V being RightMod 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