theorem Th60: :: CAT_1:65

for C, D being Category
for T being Function of the carrier' of C, the carrier' of D
for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D