for G, H being Ring
for f being Morphism of G,H holds {f} is RingMorphism_DOMAIN of G,H