:: deftheorem Def14 defines * GRCAT_1:def 16 :
for G, F being GroupMorphism st dom G = cod F holds
for b₃ being strict GroupMorphism holds
( b₃ = G * F iff for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b₃ = GroupMorphismStr(# G1,G3,(g * f) #) );