reconsider T = the carrier' of B --> (id c) as Function of the carrier' of B, the carrier' of C ;

now :: thesis: ( ( for b being Object of B ex d being Object of C st T . (id b) = id d ) & ( for f being Morphism of B holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )

thus for b being Object of B ex d being Object of C st T . (id b) = id d by FUNCOP_1:7; :: thesis: ( ( for f being Morphism of B holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
thus for f being Morphism of B holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) :: thesis: for f, g being Morphism of B st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)

proof

let f be Morphism of B; :: thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
T . (id (cod f)) = id c by FUNCOP_1:7;
then A1: T . (id (cod f)) = id (cod (id c)) ;
T . (id (dom f)) = id c by FUNCOP_1:7;
then T . (id (dom f)) = id (dom (id c)) ;
hence ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A1, FUNCOP_1:7; :: thesis: verum

end;

let f, g be Morphism of B; :: thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
assume dom g = cod f ; :: thesis: T . (g (*) f) = (T . g) (*) (T . f)
Hom (c,c) <> {} ;
then A2: ( T . f = id c & (id c) * (id c) = (id c) (*) (id c) ) by CAT_1:def 13, FUNCOP_1:7;
( T . (g (*) f) = id c & T . g = id c ) by FUNCOP_1:7;
hence T . (g (*) f) = (T . g) (*) (T . f) by A2; :: thesis: verum

end;

hence the carrier' of B --> (id c) is Functor of B,C by CAT_1:61; :: thesis: verum