theorem Th18:
for
G1,
G2,
G3 being
AddGroup for
G being
Morphism of
G2,
G3 for
F being
Morphism of
G1,
G2 for
g being
Function of
G2,
G3 for
f being
Function of
G1,
G2 st
G = GroupMorphismStr(#
G2,
G3,
g #) &
F = GroupMorphismStr(#
G1,
G2,
f #) holds
G * F = GroupMorphismStr(#
G1,
G3,
(g * f) #)