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

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

proof

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;

thus for fg being Morphism of [:C,D:] holds
( 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 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;

let fg, fg9 be Morphism of [:C,D:]; :: thesis: ( dom fg9 = cod fg implies 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;

hence pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D by CAT_1:61; :: thesis: verum