:: deftheorem defines / LMOD_7:def 23 :
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;