theorem Th83: :: CAT_1:88

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f