let D be non empty set ; :: thesis: for G, H being Ring holds
( D is RingMorphism_DOMAIN of G,H iff for x being Element of D holds x is Morphism of G,H )
let G, H be Ring; :: thesis: ( D is RingMorphism_DOMAIN of G,H iff for x being Element of D holds x is Morphism of G,H )
thus ( D is RingMorphism_DOMAIN of G,H implies for x being Element of D holds x is Morphism of G,H ) by Def14; :: thesis: ( ( for x being Element of D holds x is Morphism of G,H ) implies D is RingMorphism_DOMAIN of G,H )
thus ( ( for x being Element of D holds x is Morphism of G,H ) implies D is RingMorphism_DOMAIN of G,H ) :: thesis: verum

proof

assume A1: for x being Element of D holds x is Morphism of G,H ; :: thesis: D is RingMorphism_DOMAIN of G,H
then for x being set st x in D holds
x is strict RingMorphism ;
then reconsider D' = D as RingMorphism_DOMAIN by Def13;
for x being Element of D' holds x is Morphism of G,H by A1;
hence D is RingMorphism_DOMAIN of G,H by Def14; :: thesis: verum

end;