set F = the Morphism of G,H;
reconsider D = { the Morphism of G,H} as RingMorphism_DOMAIN by Th12;
take D ; :: thesis: for x being Element of D holds x is Morphism of G,H
thus for x being Element of D holds x is Morphism of G,H by TARSKI:def 1; :: thesis: verum