:: deftheorem defines Hom CAT_1:def 4 :
for C being non empty non void CatStr
for a, b being Object of C holds Hom (a,b) = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;