:: deftheorem defines . LMOD_7:def 18 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V . W = addLoopStr(# (V .. W),(ADD W),((0. V) .. W) #);