for G1, G2, G3 being AddGroup
for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds
G * F = GroupMorphismStr(# G1,G3,(g * f) #)