theorem Th19:
for
f,
g being
strict GroupMorphism st
dom g = cod f holds
ex
G1,
G2,
G3 being
AddGroup ex
f0 being
Function of
G1,
G2 ex
g0 being
Function of
G2,
G3 st
(
f = GroupMorphismStr(#
G1,
G2,
f0 #) &
g = GroupMorphismStr(#
G2,
G3,
g0 #) &
g * f = GroupMorphismStr(#
G1,
G3,
(g0 * f0) #) )