:: deftheorem defines AbGr LMOD_XX1:def 25 :
for R being comRing
for M being LeftMod of R holds AbGr M = addLoopStr(# the carrier of M, the addF of M,(0. M) #);