let C, D be Category; :: thesis: pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D
reconsider T = pr2 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of D ;

now

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
A1: cd = [c,d] by DOMAIN_1:9;
A2: T . ((id c),(id d)) = id d by FUNCT_3:def 6;
id cd = [(id c),(id d)] by A1, Th41;
hence ex d being Object of D st T . (id cd) = id d by A2; :: 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
A3: fg = [f,g] by DOMAIN_1:9;
T . (f,g) = T . fg by A3;
then A4: T . fg = g by FUNCT_3:def 6;
dom [f,g] = [(dom f),(dom g)] by Th38;
hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A3, Th41
.= id (dom (T . fg)) by A4, FUNCT_3:def 6 ;
:: thesis: T . (id (cod fg)) = id (cod (T . fg))
cod [f,g] = [(cod f),(cod g)] by Th38;
hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A3, Th41
.= id (cod (T . fg)) by A4, FUNCT_3:def 6 ;
:: 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 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:9;
T . (f,g) = T . fg by A6;
then A7: T . fg = g by FUNCT_3:def 6;
consider f9 being Morphism of C, g9 being Morphism of D such that
A8: fg9 = [f9,g9] by DOMAIN_1:9;
T . (f9,g9) = T . fg9 by A8;
then A9: T . fg9 = g9 by FUNCT_3:def 6;
( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th38;
then ( dom f9 = cod f & dom g9 = cod g ) by A5, A6, A8, ZFMISC_1:33;
hence T . (fg9 * fg) = T . ((f9 * f),(g9 * g)) by A6, A8, Th39
.= (T . fg9) * (T . fg) by A9, A7, FUNCT_3:def 6 ;
:: thesis: verum

end;

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