:: deftheorem defines ZERO GRCAT_1:def 12 :
for G, H being AddGroup holds ZERO (G,H) = GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);