let f be strict RingMorphism; :: thesis: {f} is RingMorphism_DOMAIN
for x being object st x in {f} holds
x is strict RingMorphism by TARSKI:def 1;
hence {f} is RingMorphism_DOMAIN by Def12; :: thesis: verum