consider G19, G299 being AddGroup such that
A8: F is Morphism of G19,G299 by Th14;
reconsider F9 = F as Morphism of G19,G299 by A8;
consider G29, G39 being AddGroup such that
A9: G is Morphism of G29,G39 by Th14;
G29 = dom G by A9, Def12;
then reconsider F9 = F9 as Morphism of G19,G29 by A1, Def12;
consider f9 being Function of G19,G29 such that
A10: GroupMorphismStr(# the Source of F9, the Target of F9, the Fun of F9 #) = GroupMorphismStr(# G19,G29,f9 #) and
f9 is additive by Th12;
reconsider G9 = G as Morphism of G29,G39 by A9;
let S1, S2 be strict GroupMorphism; :: 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
S1 = GroupMorphismStr(# G1,G3,(g * f) #) ) & ( 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
S2 = GroupMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 )
assume that
A11: 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
S1 = GroupMorphismStr(# G1,G3,(g * f) #) and
A12: 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
S2 = GroupMorphismStr(# G1,G3,(g * f) #) ; :: thesis: S1 = S2
consider g9 being Function of G29,G39 such that
A13: GroupMorphismStr(# the Source of G9, the Target of G9, the Fun of G9 #) = GroupMorphismStr(# G29,G39,g9 #) and
g9 is additive by Th12;
thus S1 = GroupMorphismStr(# G19,G39,(g9 * f9) #) by A11, A13, A10
.= S2 by A12, A13, A10 ; :: thesis: verum