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, fg' being Morphism of [:C,D:] st dom fg' = cod fg holds
T . (fg' * fg) = (T . fg') * (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: id cd = [(id c),(id d)] by A1, Th41;
T . (id c),(id d) = id d by FUNCT_3:def 6;
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, fg' being Morphism of [:C,D:] st dom fg' = cod fg holds
T . (fg' * fg) = (T . fg') * (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;
A4: ( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] ) by Th38;
T . f,g = T . fg by A3;
then A5: T . fg = g by FUNCT_3:def 6;
thus T . (id (dom fg)) = T . (id (dom f)),(id (dom g)) by A3, A4, Th41
.= id (dom (T . fg)) by A5, FUNCT_3:def 6 ; :: thesis: T . (id (cod fg)) = id (cod (T . fg))
thus T . (id (cod fg)) = T . (id (cod f)),(id (cod g)) by A3, A4, Th41
.= id (cod (T . fg)) by A5, FUNCT_3:def 6 ; :: thesis: verum

end;

let fg, fg' be Morphism of [:C,D:]; :: thesis: ( dom fg' = cod fg implies T . (fg' * fg) = (T . fg') * (T . fg) )
assume A6: dom fg' = cod fg ; :: thesis: T . (fg' * fg) = (T . fg') * (T . fg)
consider f being Morphism of C, g being Morphism of D such that
A7: fg = [f,g] by DOMAIN_1:9;
consider f' being Morphism of C, g' being Morphism of D such that
A8: fg' = [f',g'] by DOMAIN_1:9;
( dom [f',g'] = [(dom f'),(dom g')] & cod [f,g] = [(cod f),(cod g)] ) by Th38;
then A9: ( dom f' = cod f & dom g' = cod g ) by A6, A7, A8, ZFMISC_1:33;
( T . f',g' = T . fg' & T . f,g = T . fg ) by A7, A8;
then A10: ( T . fg' = g' & T . fg = g ) by FUNCT_3:def 6;
thus T . (fg' * fg) = T . (f' * f),(g' * g) by A7, A8, A9, Th39
.= (T . fg') * (T . fg) by A10, 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