for C being Category
for a being Object of C
for f being Morphism of C holds
( f in a Hom iff dom f = a )