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 )
A2: 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 ) by Lm6;
ex G1, G2' being Ring st
( G1 <= G2' & dom f = G1 & cod f = G2' & RingMorphismStr(# the Dom of f,the Cod of f,the Fun of f #) is Morphism of G1,G2' ) 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, A2; :: thesis: verum