for C being non empty composable with_identities CategoryStr
for a, b being Object of C
for f being morphism of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )