:: deftheorem defines fun GRCAT_1:def 11 :
for f being GroupMorphismStr holds fun f = the Fun of f;