consider G19, G29, G39 being AddGroup such that
A2: G is Morphism of G29,G39 and
A3: F is Morphism of G19,G29 by A1, Th16;
consider f9 being Function of G19,G29 such that
A4: GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G19,G29,f9 #) and
A5: f9 is additive by A3, Th12;
consider g9 being Function of G29,G39 such that
A6: GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G29,G39,g9 #) and
A7: g9 is additive by A2, Th12;
g9 * f9 is additive by A7, A5;
then reconsider T9 = GroupMorphismStr(# G19,G39,(g9 * f9) #) as strict GroupMorphism by Th11;
take T9 ; :: thesis: 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
T9 = GroupMorphismStr(# G1,G3,(g * f) #)
thus 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
T9 = GroupMorphismStr(# G1,G3,(g * f) #) by A6, A4; :: thesis: verum