:: deftheorem defines ID GRCAT_1:def 15 :
for G being AddGroup holds ID G = GroupMorphismStr(# G,G,(id G) #);