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 [:C,D:] ex c being Object of C st T . (id cd) = id c :: 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 c being Object of C st T . (id cd) = id c
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 c by FUNCT_3:def 5;
hence ex c being Object of C st T . (id cd) = id c 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 = f by FUNCT_3:def 5;
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 5 ; :: 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 5 ; :: 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' = f' & T . fg = f ) by FUNCT_3:def 5;
thus T . (fg' * fg) = T . (f' * f),(g' * g) by A7, A8, A9, Th39
.= (T . fg') * (T . fg) by A10, 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