:: deftheorem defines End_Ring LMOD_XX1:def 9 :
for M being AbGroup holds End_Ring M = doubleLoopStr(# (set_End M),(add_End M),(mult_End M),(1_End M),(0_End M) #);