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

now :: thesis: ( ( for cd being Object of [:C,D:] ex d being Object of D st T . (id cd) = id d ) & ( 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
pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D
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 d being Object of D st T . (id cd) = id d
:: 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 A14: 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

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

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

then A16: T . fg = g by FUNCT_3:def 5;

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

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

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

then A18: T . fg9 = g9 by FUNCT_3:def 5;

( 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 A14, A15, A17, XTUPLE_0:1;

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

.= (T . fg9) (*) (T . fg) by A18, A16, FUNCT_3:def 5 ;

:: 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 d being Object of D st T . (id cd) = id d

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

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

A11: T . ((id c),(id d)) = id d by FUNCT_3:def 5;

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

hence ex d being Object of D st T . (id cd) = id d by A11; :: thesis: verum

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

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

A11: T . ((id c),(id d)) = id d by FUNCT_3:def 5;

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

hence ex d being Object of D st T . (id cd) = id d by A11; :: 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

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

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

then A13: T . fg = g by FUNCT_3:def 5;

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

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

.= id (dom (T . fg)) by A13, FUNCT_3:def 5 ;

:: 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 A12, Th25

.= id (cod (T . fg)) by A13, FUNCT_3:def 5 ;

:: thesis: verum

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

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

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

then A13: T . fg = g by FUNCT_3:def 5;

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

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

.= id (dom (T . fg)) by A13, FUNCT_3:def 5 ;

:: 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 A12, Th25

.= id (cod (T . fg)) by A13, FUNCT_3:def 5 ;

:: thesis: verum

assume A14: 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

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

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

then A16: T . fg = g by FUNCT_3:def 5;

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

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

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

then A18: T . fg9 = g9 by FUNCT_3:def 5;

( 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 A14, A15, A17, XTUPLE_0:1;

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

.= (T . fg9) (*) (T . fg) by A18, A16, FUNCT_3:def 5 ;

:: thesis: verum