:: deftheorem defines 1_End LMOD_XX1:def 7 :
for M being AbGroup holds 1_End M = id M;