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) ) )

hence
the carrier' of B --> (id c) is Functor of B,C
by CAT_1:61; :: thesis: verum( 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)

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;( 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, g be Morphism of B; :: thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
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;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

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