theorem :: ZMODUL01:31

for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V
for w1, w2 being Vector of W st w1 = v & w2 = u holds
w1 - w2 = v - u by VECTSP_4:16;