set G0 = the Element of V;
set M = Morphs ( the Element of V, the Element of V);
set S = { (Morphs (G,H)) where G, H is Element of V : G <= H } ;
( ID the Element of V is Element of Morphs ( the Element of V, the Element of V) & Morphs ( the Element of V, the Element of V) in { (Morphs (G,H)) where G, H is Element of V : G <= H } ) by Def14;
then reconsider T = union { (Morphs (G,H)) where G, H is Element of V : G <= H } as non empty set by TARSKI:def 4;
A1: for x being object holds
( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )

proof

let x be object ; :: thesis: ( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus ( x in T implies ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) :: thesis: ( ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) implies x in T )

proof

assume x in T ; :: thesis: ex G, H being Element of V st
( G <= H & x is Morphism of G,H )
then consider Y being set such that
A2: x in Y and
A3: Y in { (Morphs (G,H)) where G, H is Element of V : G <= H } by TARSKI:def 4;
consider G, H being Element of V such that
A4: Y = Morphs (G,H) and
A5: G <= H by A3;
take G ; :: thesis: ex H being Element of V st
( G <= H & x is Morphism of G,H )
take H ; :: thesis: ( G <= H & x is Morphism of G,H )
x is Element of Morphs (G,H) by A2, A4;
hence ( G <= H & x is Morphism of G,H ) by A5; :: thesis: verum

end;

thus ( ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) implies x in T ) :: thesis: verum

proof

given G, H being Element of V such that A6: ( G <= H & x is Morphism of G,H ) ; :: thesis: x in T
set M = Morphs (G,H);
( x in Morphs (G,H) & Morphs (G,H) in { (Morphs (G,H)) where G, H is Element of V : G <= H } ) by A6, Def14;
hence x in T by TARSKI:def 4; :: thesis: verum

end;

end;

now :: thesis: for x being object st x in T holds
x is strict RingMorphism

let x be object ; :: thesis: ( x in T implies x is strict RingMorphism )
assume x in T ; :: thesis: x is strict RingMorphism
then ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) by A1;
hence x is strict RingMorphism ; :: thesis: verum

end;

then reconsider T9 = T as RingMorphism_DOMAIN by Def12;
take T9 ; :: thesis: for x being object holds
( x in T9 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus for x being object holds
( x in T9 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) by A1; :: thesis: verum