:: deftheorem Def12 defines RingMorphism_DOMAIN-like RINGCAT1:def 12 :
for IT being set holds
( IT is RingMorphism_DOMAIN-like iff for x being object st x in IT holds
x is strict RingMorphism );