reconsider T = pr1 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of C ;

now :: thesis: ( ( for cd being Object of [:C,D:] ex c being Object of C st T . (id cd) = id c ) & ( for fg being Morphism of [:C,D:] holds

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds

T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )

hence
pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C
by CAT_1:61; :: thesis: verum( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds

T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )

thus
for cd being Object of [:C,D:] ex c being Object of C st T . (id cd) = id c
:: thesis: ( ( for fg being Morphism of [:C,D:] holds

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds

T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis: for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds

T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)

assume A5: dom fg9 = cod fg ; :: thesis: T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)

consider f being Morphism of C, g being Morphism of D such that

A6: fg = [f,g] by DOMAIN_1:1;

T . (f,g) = T . fg by A6;

then A7: T . fg = f by FUNCT_3:def 4;

consider f9 being Morphism of C, g9 being Morphism of D such that

A8: fg9 = [f9,g9] by DOMAIN_1:1;

T . (f9,g9) = T . fg9 by A8;

then A9: T . fg9 = f9 by FUNCT_3:def 4;

( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th22;

then ( dom f9 = cod f & dom g9 = cod g ) by A5, A6, A8, XTUPLE_0:1;

hence T . (fg9 (*) fg) = T . ((f9 (*) f),(g9 (*) g)) by A6, A8, Th23

.= (T . fg9) (*) (T . fg) by A9, A7, FUNCT_3:def 4 ;

:: thesis: verum

end;( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds

T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )

proof

thus
for fg being Morphism of [:C,D:] holds
let cd be Object of [:C,D:]; :: thesis: ex c being Object of C st T . (id cd) = id c

consider c being Object of C, d being Object of D such that

A1: cd = [c,d] by DOMAIN_1:1;

A2: T . ((id c),(id d)) = id c by FUNCT_3:def 4;

id cd = [(id c),(id d)] by A1, Th25;

hence ex c being Object of C st T . (id cd) = id c by A2; :: thesis: verum

end;consider c being Object of C, d being Object of D such that

A1: cd = [c,d] by DOMAIN_1:1;

A2: T . ((id c),(id d)) = id c by FUNCT_3:def 4;

id cd = [(id c),(id d)] by A1, Th25;

hence ex c being Object of C st T . (id cd) = id c by A2; :: thesis: verum

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis: for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds

T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)

proof

let fg, fg9 be Morphism of [:C,D:]; :: thesis: ( dom fg9 = cod fg implies T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) )
let fg be Morphism of [:C,D:]; :: thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )

consider f being Morphism of C, g being Morphism of D such that

A3: fg = [f,g] by DOMAIN_1:1;

T . (f,g) = T . fg by A3;

then A4: T . fg = f by FUNCT_3:def 4;

dom [f,g] = [(dom f),(dom g)] by Th22;

hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A3, Th25

.= id (dom (T . fg)) by A4, FUNCT_3:def 4 ;

:: thesis: T . (id (cod fg)) = id (cod (T . fg))

cod [f,g] = [(cod f),(cod g)] by Th22;

hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A3, Th25

.= id (cod (T . fg)) by A4, FUNCT_3:def 4 ;

:: thesis: verum

end;consider f being Morphism of C, g being Morphism of D such that

A3: fg = [f,g] by DOMAIN_1:1;

T . (f,g) = T . fg by A3;

then A4: T . fg = f by FUNCT_3:def 4;

dom [f,g] = [(dom f),(dom g)] by Th22;

hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A3, Th25

.= id (dom (T . fg)) by A4, FUNCT_3:def 4 ;

:: thesis: T . (id (cod fg)) = id (cod (T . fg))

cod [f,g] = [(cod f),(cod g)] by Th22;

hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A3, Th25

.= id (cod (T . fg)) by A4, FUNCT_3:def 4 ;

:: thesis: verum

assume A5: dom fg9 = cod fg ; :: thesis: T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)

consider f being Morphism of C, g being Morphism of D such that

A6: fg = [f,g] by DOMAIN_1:1;

T . (f,g) = T . fg by A6;

then A7: T . fg = f by FUNCT_3:def 4;

consider f9 being Morphism of C, g9 being Morphism of D such that

A8: fg9 = [f9,g9] by DOMAIN_1:1;

T . (f9,g9) = T . fg9 by A8;

then A9: T . fg9 = f9 by FUNCT_3:def 4;

( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th22;

then ( dom f9 = cod f & dom g9 = cod g ) by A5, A6, A8, XTUPLE_0:1;

hence T . (fg9 (*) fg) = T . ((f9 (*) f),(g9 (*) g)) by A6, A8, Th23

.= (T . fg9) (*) (T . fg) by A9, A7, FUNCT_3:def 4 ;

:: thesis: verum