let G1, G2, G3 be AddGroup; 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; for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3
let F be Morphism of G1,G2; 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 Th12;
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 Th12;
dom G =
G2
by Def12
.=
cod F
by Def12
;
then
G * F = GroupMorphismStr(# G1,G3,(g * f) #)
by A1, A2, Def14;
then
( dom (G * F) = G1 & cod (G * F) = G3 )
;
hence
G * F is Morphism of G1,G3
by Def12; verum