theorem :: LMOD_7:16

for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 . W = a2 . W iff a1 - a2 in W ) by Th11;