defpred S1[ RingMorphism, RingMorphism] means dom $1 = cod $2;
let g, f be RingMorphism; ( 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:
S1[g,f]
; 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; verum