:: deftheorem defines ID MOD_2:def 9 :
for R being Ring
for G being LeftMod of R holds ID G = LModMorphismStr(# G,G,(id G) #);