defpred S₁[ RingMorphism, RingMorphism] means dom $1 = cod $2;
let g, f be RingMorphism; :: thesis: ( dom g = cod f implies 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 ) )
assume A1: S₁[g,f] ; :: thesis: 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 )
( ex G2, G3 being Ring st
( G2 <= G3 & dom g = G2 & cod g = G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 ) & ex G1, G29 being Ring st
( G1 <= G29 & dom f = G1 & cod f = G29 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G29 ) ) by Lm6;
hence 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 ) by A1; :: thesis: verum