let V be Ring_DOMAIN; :: thesis: for g, f being Element of Morphs V st dom g = cod f holds
ex G1, G2, G3 being Element of V st
( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 )
set X = Morphs V;
defpred S₁[ Element of Morphs V, Element of Morphs V] means dom $1 = cod $2;
let g, f be Element of Morphs V; :: thesis: ( dom g = cod f implies ex G1, G2, G3 being Element of V st
( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1: S₁[g,f] ; :: thesis: ex G1, G2, G3 being Element of V st
( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 )
consider G2, G3 being Element of V such that
A2: G2 <= G3 and
A3: g is Morphism of G2,G3 by Def18;
A4: G2 = dom g by A2, A3, Def9;
consider G1, G2' being Element of V such that
A5: G1 <= G2' and
A6: f is Morphism of G1,G2' by Def18;
G2' = cod f by A5, A6, Def9;
hence ex G1, G2, G3 being Element of V st
( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4, A5, A6; :: thesis: verum