:: deftheorem defines hom CAT_1:def 28 :
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds hom (T,c,c9) = T | (Hom (c,c9));