let D be non empty set ; 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; ( 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 Def13; ( ( 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 )
verum