for f being GroupMorphismStr
for G1, G2 being AddGroup
for f0 being Function of G1,G2 st f = GroupMorphismStr(# G1,G2,f0 #) holds
( dom f = G1 & cod f = G2 & fun f = f0 ) ;