theorem Th82: :: CAT_1:87

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))