:: deftheorem defines fun RINGCAT1:def 4 :
for f being RingMorphismStr holds fun f = the Fun of f;