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