let C be Category; :: thesis: id the carrier' of C is Functor of C,C
set F = id the carrier of C;
set T = id the carrier' of C;
( ( for c being Object of C holds (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) ) & ( for f being Morphism of C holds
( (id the carrier of C) . (dom f) = dom ((id the carrier' of C) . f) & (id the carrier of C) . (cod f) = cod ((id the carrier' of C) . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(id the carrier' of C) . (g (*) f) = ((id the carrier' of C) . g) (*) ((id the carrier' of C) . f) ) ) ;
hence id the carrier' of C is Functor of C,C by Th60; :: thesis: verum