:: deftheorem defines dom RINGCAT1:def 2 :
for f being RingMorphismStr holds dom f = the DomR of f;