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

now

thus for cd being Object of ex c being Object of st T . (id cd) = id c :: thesis: ( ( for fg being Morphism of holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg' being Morphism of st dom fg' = cod fg holds
T . (fg' * fg) = (T . fg') * (T . fg) ) )

proof

let cd be Object of ; :: thesis: ex c being Object of st T . (id cd) = id c
consider c being Object of , d being Object of such that
A1: cd = [c,d] by DOMAIN_1:9;
A2: T . (id c),(id d) = id c by FUNCT_3:def 5;
id cd = [(id c),(id d)] by A1, Th41;
hence ex c being Object of st T . (id cd) = id c by A2; :: thesis: verum

end;

thus for fg being Morphism of holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis: for fg, fg' being Morphism of st dom fg' = cod fg holds
T . (fg' * fg) = (T . fg') * (T . fg)

proof

let fg be Morphism of ; :: thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being Morphism of , g being Morphism of such that
A3: fg = [f,g] by DOMAIN_1:9;
T . f,g = T . fg by A3;
then A4: T . fg = f by FUNCT_3:def 5;
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 5 ;
:: 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 5 ;
:: thesis: verum

end;

let fg, fg' be Morphism of ; :: thesis: ( dom fg' = cod fg implies T . (fg' * fg) = (T . fg') * (T . fg) )
assume A5: dom fg' = cod fg ; :: thesis: T . (fg' * fg) = (T . fg') * (T . fg)
consider f being Morphism of , g being Morphism of such that
A6: fg = [f,g] by DOMAIN_1:9;
T . f,g = T . fg by A6;
then A7: T . fg = f by FUNCT_3:def 5;
consider f' being Morphism of , g' being Morphism of such that
A8: fg' = [f',g'] by DOMAIN_1:9;
T . f',g' = T . fg' by A8;
then A9: T . fg' = f' by FUNCT_3:def 5;
( dom [f',g'] = [(dom f'),(dom g')] & cod [f,g] = [(cod f),(cod g)] ) by Th38;
then ( dom f' = cod f & dom g' = cod g ) by A5, A6, A8, ZFMISC_1:33;
hence T . (fg' * fg) = T . (f' * f),(g' * g) by A6, A8, Th39
.= (T . fg') * (T . fg) by A9, A7, FUNCT_3:def 5 ;
:: thesis: verum

end;

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