consider G1', G2', G3' being AddGroup such that
A2: G is Morphism of G2',G3' and
A3: F is Morphism of G1',G2' by A1, Th26;
consider g' being Function of G2',G3' such that
A4: GroupMorphismStr(# the Source of G,the Target of G,the Fun of G #) = GroupMorphismStr(# G2',G3',g' #) and
A5: g' is additive by A2, Th22;
consider f' being Function of G1',G2' such that
A6: GroupMorphismStr(# the Source of F,the Target of F,the Fun of F #) = GroupMorphismStr(# G1',G2',f' #) and
A7: f' is additive by A3, Th22;
g' * f' is additive by A5, A7, Th14;
then reconsider T' = GroupMorphismStr(# G1',G3',(g' * f') #) as strict GroupMorphism by Th20;
take T' ; :: 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
T' = 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
T' = GroupMorphismStr(# G1,G3,(g * f) #) by A4, A6; :: thesis: verum