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

thus for b being Object of B ex d being Object of C st T . (id b) = id d by FUNCOP_1:7; :: thesis:
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:

let f be Morphism of B; :: thesis:
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:

end;

let f, g be Morphism of B; :: thesis:
assume dom g = cod f ; :: thesis:
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:

end;