:: deftheorem defines AbGrLMod LMOD_XX1:def 13 :
for R being Ring
for M being AbGroup
for s being Function of R,(End_Ring M) holds AbGrLMod (M,s) = ModuleStr(# the carrier of M, the addF of M,(0. M),(LModlmult (M,s)) #);