theorem Th2: :: RINGCAT1:2

for g, f being RingMorphism st dom g = cod f holds
ex G1, G2, G3 being Ring st
( G1 <= G2 & G2 <= G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 )