for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )