theorem Th7:
for
f,
g being
strict RingMorphism st
dom g = cod f holds
ex
G1,
G2,
G3 being
Ring ex
f0 being
Function of
G1,
G2 ex
g0 being
Function of
G2,
G3 st
(
f = RingMorphismStr(#
G1,
G2,
f0 #) &
g = RingMorphismStr(#
G2,
G3,
g0 #) &
g * f = RingMorphismStr(#
G1,
G3,
(g0 * f0) #) )