:: deftheorem defines .. LMOD_7:def 13 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for a being Vector of V holds a .. W = a + W;