for C being Category
for f being Morphism of C holds
( f in (dom f) Hom & f in Hom (cod f) ) by Th23, Th24;