:: deftheorem Def2 defines Hom CAT_7:def 2 :
for C being non empty composable with_identities CategoryStr
for a, b being Object of C holds Hom (a,b) = { f where f is morphism of C : ( dom f = a & cod f = b ) } ;