let D1, D2 be RingMorphism_DOMAIN; :: thesis: ( ( for x being object holds
( x in D1 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ) & ( for x being object holds
( x in D2 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ) implies D1 = D2 )
assume that
A7: for x being object holds
( x in D1 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) and
A8: for x being object holds
( x in D2 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ; :: thesis: D1 = D2

now :: thesis: for x being object holds
( x in D1 iff x in D2 )

let x be object ; :: thesis: ( x in D1 iff x in D2 )
( x in D1 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) by A7;
hence ( x in D1 iff x in D2 ) by A8; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum