:: deftheorem Def5 defines RingMorphism-like RINGCAT1:def 5 :
for IT being RingMorphismStr holds
( IT is RingMorphism-like iff fun IT is linear );