let G1, G2, G3 be AddGroup; :: thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3
let G be Morphism of G2,G3; :: thesis: for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3
let F be Morphism of G1,G2; :: thesis: G * F is Morphism of G1,G3
consider g being Function of G2,G3 such that
A1: GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) and
g is additive by Th22;
consider f being Function of G1,G2 such that
A2: GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) and
f is additive by Th22;
dom G = G2 by Def19
.= cod F by Def19 ;
then G * F = GroupMorphismStr(# G1,G3,(g * f) #) by A1, A2, Def21;
then ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
hence G * F is Morphism of G1,G3 by Def19; :: thesis: verum