:: deftheorem defines Hom CAT_5:def 9 :
for C being Category
for o being Object of C holds Hom o = the Target of C " {o};