consider G1', G2'' being AddGroup such that
A8: F is Morphism of G1',G2'' by Th24;
reconsider F' = F as Morphism of G1',G2'' by A8;
consider G2', G3' being AddGroup such that
A9: G is Morphism of G2',G3' by Th24;
G2' = dom G by A9, Def19;
then reconsider F' = F' as Morphism of G1',G2' by A1, Def19;
consider f' being Function of G1',G2' such that
A10: GroupMorphismStr(# the Source of F',the Target of F',the Fun of F' #) = GroupMorphismStr(# G1',G2',f' #) and
f' is additive by Th22;
reconsider G' = G as Morphism of G2',G3' 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 g' being Function of G2',G3' such that
A13: GroupMorphismStr(# the Source of G',the Target of G',the Fun of G' #) = GroupMorphismStr(# G2',G3',g' #) and
g' is additive by Th22;
thus S1 = GroupMorphismStr(# G1',G3',(g' * f') #) by A11, A13, A10
.= S2 by A12, A13, A10 ; :: thesis: verum