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;

now

thus for c being Object of C holds (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) :: thesis: ( ( 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) ) )

proof

let c be Object of C; :: thesis: (id the carrier' of C) . (id c) = id ((id the carrier of C) . c)
(id the carrier of C) . c = c by FUNCT_1:18;
hence (id the carrier' of C) . (id c) = id ((id the carrier of C) . c) by FUNCT_1:18; :: thesis: verum

end;

thus 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) ) :: thesis: 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)

proof

let f be Morphism of C; :: thesis: ( (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) )
(id the carrier' of C) . f = f by FUNCT_1:18;
hence ( (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) ) by FUNCT_1:18; :: thesis: verum

end;

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies (id the carrier' of C) . (g * f) = ((id the carrier' of C) . g) * ((id the carrier' of C) . f) )
assume dom g = cod f ; :: thesis: (id the carrier' of C) . (g * f) = ((id the carrier' of C) . g) * ((id the carrier' of C) . f)
thus (id the carrier' of C) . (g * f) = g * f by FUNCT_1:18
.= ((id the carrier' of C) . g) * f by FUNCT_1:18
.= ((id the carrier' of C) . g) * ((id the carrier' of C) . f) by FUNCT_1:18 ; :: thesis: verum

end;

hence id the carrier' of C is Functor of C,C by Th100; :: thesis: verum