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 ;
( 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 ) )
( 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
;
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
;
ex H being Element of V st
( G <= H & x is Morphism of G,H )
take
H
;
( 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;
verum
end;
thus
( ex
G,
H being
Element of
V st
(
G <= H &
x is
Morphism of
G,
H ) implies
x in T )
verum
end;
then reconsider T9 = T as RingMorphism_DOMAIN by Def12;
take
T9
; 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; verum