let C, C1, C2 be category; :: thesis:
let F1 be Functor of C1,C; :: thesis:
let F2 be Functor of C2,C; :: thesis:
assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis:
reconsider car = { [f1,f2] where f1 is morphism of C1, f2 is morphism of C2 : ( f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) } as set ;
set comp = { [[x1,x2],x3] where x1, x2, x3 is Element of car : ( x1 in car & x2 in car & x3 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] & x3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } ;
for x being object st x in { [[x1,x2],x3] where x1, x2, x3 is Element of car : ( x1 in car & x2 in car & x3 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] & x3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } holds
x in [:[:car,car:],car:]

let x be object ; :: thesis:
assume x in { [[x1,x2],x3] where x1, x2, x3 is Element of car : ( x1 in car & x2 in car & x3 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] & x3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } ; :: thesis:
then consider x1, x2, x3 being Element of car such that
A2: ( x = [[x1,x2],x3] & x1 in car & x2 in car & x3 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] & x3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) ;
[x1,x2] in [:car,car:] by A2, ZFMISC_1:def 2;
hence x in [:[:car,car:],car:] by A2, ZFMISC_1:def 2; :: thesis:

end;

then reconsider comp = { [[x1,x2],x3] where x1, x2, x3 is Element of car : ( x1 in car & x2 in car & x3 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] & x3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } as Relation of [:car,car:],car by TARSKI:def 3;
for x, y1, y2 being object st [x,y1] in comp & [x,y2] in comp holds
y1 = y2

let x, y1, y2 be object ; :: thesis:
assume [x,y1] in comp ; :: thesis:
then consider x11, x12, x13 being Element of car such that
A3: ( [x,y1] = [[x11,x12],x13] & x11 in car & x12 in car & x13 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x11 = [f11,f21] & x12 = [f12,f22] & x13 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) ;
assume [x,y2] in comp ; :: thesis:
then consider x21, x22, x23 being Element of car such that
A4: ( [x,y2] = [[x21,x22],x23] & x21 in car & x22 in car & x23 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x21 = [f11,f21] & x22 = [f12,f22] & x23 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) ;
A5: ( x = [x11,x12] & y1 = x13 ) by A3, XTUPLE_0:1;
A6: ( x = [x21,x22] & y2 = x23 ) by A4, XTUPLE_0:1;
A7: ( x11 = x21 & x12 = x22 ) by A5, A6, XTUPLE_0:1;
consider f11 being morphism of C1, f21 being morphism of C2 such that
A8: ( x11 = [f11,f21] & f11 in the carrier of C1 & f21 in the carrier of C2 & F1 . f11 = F2 . f21 ) by A3;
consider f12 being morphism of C1, f22 being morphism of C2 such that
A9: ( x12 = [f12,f22] & f12 in the carrier of C1 & f22 in the carrier of C2 & F1 . f12 = F2 . f22 ) by A3;
consider f13 being morphism of C1, f23 being morphism of C2 such that
A10: ( x13 = [f13,f23] & f13 in the carrier of C1 & f23 in the carrier of C2 & F1 . f13 = F2 . f23 ) by A3;
consider f213 being morphism of C1, f223 being morphism of C2 such that
A11: ( x23 = [f213,f223] & f213 in the carrier of C1 & f223 in the carrier of C2 & F1 . f213 = F2 . f223 ) by A4;
A12: ( f13 = f11 (*) f12 & f23 = f21 (*) f22 ) by A3, A8, A9, A10;
( f213 = f11 (*) f12 & f223 = f21 (*) f22 ) by A8, A9, A11, A4, A7;
hence y1 = y2 by A6, A12, A10, A11, A3, XTUPLE_0:1; :: thesis:

end;

then reconsider comp = comp as PartFunc of [:car,car:],car by FUNCT_1:def 1;
set D = CategoryStr(# car,comp #);
A13: for g1, g2 being morphism of CategoryStr(# car,comp #) st g1 |> g2 holds
ex f11, f12, f13 being morphism of C1 ex f21, f22, f23 being morphism of C2 st
( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g1 (*) g2 = [f13,f23] )

let g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis:
assume A14: g1 |> g2 ; :: thesis:
g1 in the carrier of CategoryStr(# car,comp #) by A14, Th1, CAT_6:1;
then consider f11 being morphism of C1, f21 being morphism of C2 such that
A15: ( g1 = [f11,f21] & f11 in the carrier of C1 & f21 in the carrier of C2 & F1 . f11 = F2 . f21 ) ;
g2 in the carrier of CategoryStr(# car,comp #) by A14, Th1, CAT_6:1;
then consider f12 being morphism of C1, f22 being morphism of C2 such that
A16: ( g2 = [f12,f22] & f12 in the carrier of C1 & f22 in the carrier of C2 & F1 . f12 = F2 . f22 ) ;
[g1,g2] in dom the composition of CategoryStr(# car,comp #) by A14, CAT_6:def 2;
then consider y being object such that
A17: [[g1,g2],y] in comp by XTUPLE_0:def 12;
consider x1, x2, x3 being Element of car such that
A18: ( [[g1,g2],y] = [[x1,x2],x3] & x1 in car & x2 in car & x3 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] & x3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) by A17;
consider f13 being morphism of C1, f23 being morphism of C2 such that
A19: ( x3 = [f13,f23] & f13 in the carrier of C1 & f23 in the carrier of C2 & F1 . f13 = F2 . f23 ) by A18;
( [x1,x2] = [g1,g2] & y = x3 ) by A18, XTUPLE_0:1;
then A20: ( x1 = g1 & x2 = g2 ) by XTUPLE_0:1;
take f11 ; :: thesis:
take f12 ; :: thesis:
take f13 ; :: thesis:
take f21 ; :: thesis:
take f22 ; :: thesis:
take f23 ; :: thesis:
thus ( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 ) by A15, A16; :: thesis:
thus ( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) by A20, A18, A19, A15, A16; :: thesis:
thus g1 (*) g2 = the composition of CategoryStr(# car,comp #) . (g1,g2) by A14, CAT_6:def 3
.= the composition of CategoryStr(# car,comp #) . [g1,g2] by BINOP_1:def 1
.= y by A17, FUNCT_1:1
.= [f13,f23] by A19, A18, XTUPLE_0:1 ; :: thesis:

end;

A21: ( F1 is multiplicative & F2 is multiplicative ) by A1, CAT_6:def 25;
A22: for g1, g2 being morphism of CategoryStr(# car,comp #) st ex f11, f12 being morphism of C1 ex f21, f22 being morphism of C2 st
( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 ) holds
g1 |> g2

let g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis:
given f11, f12 being morphism of C1, f21, f22 being morphism of C2 such that A23: ( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 ) ; :: thesis:
set x3 = [(f11 (*) f12),(f21 (*) f22)];
A24: ( f11 in the carrier of C1 & f12 in the carrier of C1 & f21 in the carrier of C2 & f22 in the carrier of C2 ) by A23, Th1, CAT_6:1;
A25: ( f11 (*) f12 in the carrier of C1 & f21 (*) f22 in the carrier of C2 ) by A23, Th1, CAT_6:1;
F1 . (f11 (*) f12) = (F1 . f11) (*) (F1 . f12) by A21, A23, CAT_6:def 23
.= F2 . (f21 (*) f22) by A21, A23, CAT_6:def 23 ;
then [(f11 (*) f12),(f21 (*) f22)] in car by A25;
then reconsider g3 = [(f11 (*) f12),(f21 (*) f22)] as morphism of CategoryStr(# car,comp #) by CAT_6:def 1;
reconsider x1 = g1, x2 = g2, x3 = g3 as Element of car by CAT_6:def 1;
A26: ( x1 in car & x2 in car ) by A23, A24;
for f011, f012, f013 being morphism of C1
for f021, f022, f023 being morphism of C2 st x1 = [f011,f021] & x2 = [f012,f022] & x3 = [f013,f023] holds
( f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 )

let f011, f012, f013 be morphism of C1; :: thesis:
let f021, f022, f023 be morphism of C2; :: thesis:
assume ( x1 = [f011,f021] & x2 = [f012,f022] & x3 = [f013,f023] ) ; :: thesis:
then ( f11 = f011 & f21 = f021 & f12 = f012 & f22 = f022 & f11 (*) f12 = f013 & f21 (*) f22 = f023 ) by A23, XTUPLE_0:1;
hence ( f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 ) by A23; :: thesis:

end;

then [[x1,x2],x3] in the composition of CategoryStr(# car,comp #) by A26;
then [g1,g2] in dom the composition of CategoryStr(# car,comp #) by XTUPLE_0:def 12;
hence g1 |> g2 by CAT_6:def 2; :: thesis:

end;

for g, g1, g2 being morphism of CategoryStr(# car,comp #) st g1 |> g2 holds
( g1 (*) g2 |> g iff g2 |> g )

let g, g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis:
assume g1 |> g2 ; :: thesis:
then consider f11, f12, f13 being morphism of C1, f21, f22, f23 being morphism of C2 such that
A27: ( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g1 (*) g2 = [f13,f23] ) by A13;

hereby :: thesis:

assume g1 (*) g2 |> g ; :: thesis:
then consider f011, f012, f013 being morphism of C1, f021, f022, f023 being morphism of C2 such that
A28: ( g1 (*) g2 = [f011,f021] & g = [f012,f022] & F1 . f011 = F2 . f021 & F1 . f012 = F2 . f022 & f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 & (g1 (*) g2) (*) g = [f013,f023] ) by A13;
A29: ( f13 = f011 & f23 = f021 ) by A27, A28, XTUPLE_0:1;
( C1 is left_composable & C2 is left_composable ) by CAT_6:def 11;
then ( f12 |> f012 & f22 |> f022 ) by A27, A28, A29, CAT_6:def 8;
hence g2 |> g by A22, A27, A28; :: thesis:

end;

assume g2 |> g ; :: thesis:
then consider f011, f012, f013 being morphism of C1, f021, f022, f023 being morphism of C2 such that
A30: ( g2 = [f011,f021] & g = [f012,f022] & F1 . f011 = F2 . f021 & F1 . f012 = F2 . f022 & f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 & g2 (*) g = [f013,f023] ) by A13;
A31: ( f12 = f011 & f22 = f021 ) by A27, A30, XTUPLE_0:1;
( C1 is left_composable & C2 is left_composable ) by CAT_6:def 11;
then A32: ( f13 |> f012 & f23 |> f022 ) by A27, A30, A31, CAT_6:def 8;
F1 . f13 = (F1 . f11) (*) (F1 . f12) by A21, A27, CAT_6:def 23
.= F2 . f23 by A21, A27, CAT_6:def 23 ;
hence g1 (*) g2 |> g by A22, A27, A30, A32; :: thesis:

end;

then A33: CategoryStr(# car,comp #) is left_composable by CAT_6:def 8;
A34: for g, g1, g2 being morphism of CategoryStr(# car,comp #) st g1 |> g2 holds
( g |> g1 (*) g2 iff g |> g1 )

let g, g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis:
assume g1 |> g2 ; :: thesis:
then consider f11, f12, f13 being morphism of C1, f21, f22, f23 being morphism of C2 such that
A35: ( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g1 (*) g2 = [f13,f23] ) by A13;

hereby :: thesis:

assume g |> g1 (*) g2 ; :: thesis:
then consider f011, f012, f013 being morphism of C1, f021, f022, f023 being morphism of C2 such that
A36: ( g = [f011,f021] & g1 (*) g2 = [f012,f022] & F1 . f011 = F2 . f021 & F1 . f012 = F2 . f022 & f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 & g (*) (g1 (*) g2) = [f013,f023] ) by A13;
A37: ( f13 = f012 & f23 = f022 ) by A35, A36, XTUPLE_0:1;
( C1 is right_composable & C2 is right_composable ) by CAT_6:def 11;
then ( f011 |> f11 & f021 |> f21 ) by A35, A36, A37, CAT_6:def 9;
hence g |> g1 by A22, A35, A36; :: thesis:

end;

assume g |> g1 ; :: thesis:
then consider f011, f012, f013 being morphism of C1, f021, f022, f023 being morphism of C2 such that
A38: ( g = [f011,f021] & g1 = [f012,f022] & F1 . f011 = F2 . f021 & F1 . f012 = F2 . f022 & f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 & g (*) g1 = [f013,f023] ) by A13;
A39: ( f11 = f012 & f21 = f022 ) by A35, A38, XTUPLE_0:1;
( C1 is right_composable & C2 is right_composable ) by CAT_6:def 11;
then A40: ( f011 |> f13 & f021 |> f23 ) by A35, A38, A39, CAT_6:def 9;
F1 . f13 = (F1 . f11) (*) (F1 . f12) by A21, A35, CAT_6:def 23
.= F2 . f23 by A21, A35, CAT_6:def 23 ;
hence g |> g1 (*) g2 by A22, A35, A38, A40; :: thesis:

end;

for g1 being morphism of CategoryStr(# car,comp #) st g1 in the carrier of CategoryStr(# car,comp #) holds
ex g being morphism of CategoryStr(# car,comp #) st
( g |> g1 & g is left_identity )

let g1 be morphism of CategoryStr(# car,comp #); :: thesis:
assume g1 in the carrier of CategoryStr(# car,comp #) ; :: thesis:
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A41: ( g1 = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) ;
A42: not C1 is empty by A41;
A43: cod f1 in the carrier of C1 by A42, Th2;
then reconsider c1 = cod f1 as morphism of C1 by CAT_6:def 1;
A44: not C2 is empty by A41;
A45: cod f2 in the carrier of C2 by A44, Th2;
then reconsider c2 = cod f2 as morphism of C2 by CAT_6:def 1;
A46: not C is empty by A1, A42, CAT_6:31;
set g = [c1,c2];
A47: F1 . c1 = F1 . (cod f1) by A42, CAT_6:def 21
.= cod (F1 . f1) by A42, A46, A1, CAT_6:32
.= F2 . (cod f2) by A41, A44, A46, A1, CAT_6:32
.= F2 . c2 by A44, CAT_6:def 21 ;
then [c1,c2] in car by A43, A45;
then reconsider g = [c1,c2] as morphism of CategoryStr(# car,comp #) by CAT_6:def 1;
take g ; :: thesis:
consider c11 being morphism of C1 such that
A48: ( c1 = c11 & c11 |> f1 & c11 is identity ) by A42, CAT_6:def 19;
consider c22 being morphism of C2 such that
A49: ( c2 = c22 & c22 |> f2 & c22 is identity ) by A44, CAT_6:def 19;
thus g |> g1 by A22, A47, A41, A48, A49; :: thesis:
for g1 being morphism of CategoryStr(# car,comp #) st g |> g1 holds
g (*) g1 = g1

let g1 be morphism of CategoryStr(# car,comp #); :: thesis:
assume g |> g1 ; :: thesis:
then consider f11, f12, f13 being morphism of C1, f21, f22, f23 being morphism of C2 such that
A50: ( g = [f11,f21] & g1 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g (*) g1 = [f13,f23] ) by A13;
A51: ( c11 = f11 & c22 = f21 ) by A48, A49, A50, XTUPLE_0:1;
( f13 = f12 & f23 = f22 ) by A51, A50, CAT_6:def 4, A48, A49, CAT_6:def 14;
hence g (*) g1 = g1 by A50; :: thesis:

end;

hence g is left_identity by CAT_6:def 4; :: thesis:

end;

then A52: CategoryStr(# car,comp #) is with_left_identities by CAT_6:def 6;
A53: for g1 being morphism of CategoryStr(# car,comp #) st g1 in the carrier of CategoryStr(# car,comp #) holds
ex g being morphism of CategoryStr(# car,comp #) st
( g1 |> g & g is right_identity )

let g1 be morphism of CategoryStr(# car,comp #); :: thesis:
assume g1 in the carrier of CategoryStr(# car,comp #) ; :: thesis:
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A54: ( g1 = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) ;
A55: not C1 is empty by A54;
A56: dom f1 in the carrier of C1 by A55, Th2;
then reconsider d1 = dom f1 as morphism of C1 by CAT_6:def 1;
A57: not C2 is empty by A54;
A58: dom f2 in the carrier of C2 by A57, Th2;
then reconsider d2 = dom f2 as morphism of C2 by CAT_6:def 1;
A59: not C is empty by A1, A55, CAT_6:31;
set g = [d1,d2];
A60: F1 . d1 = F1 . (dom f1) by A55, CAT_6:def 21
.= dom (F1 . f1) by A55, A59, A1, CAT_6:32
.= F2 . (dom f2) by A54, A57, A59, A1, CAT_6:32
.= F2 . d2 by A57, CAT_6:def 21 ;
then [d1,d2] in car by A56, A58;
then reconsider g = [d1,d2] as morphism of CategoryStr(# car,comp #) by CAT_6:def 1;
take g ; :: thesis:
consider d11 being morphism of C1 such that
A61: ( d1 = d11 & f1 |> d11 & d11 is identity ) by A55, CAT_6:def 18;
consider d22 being morphism of C2 such that
A62: ( d2 = d22 & f2 |> d22 & d22 is identity ) by A57, CAT_6:def 18;
thus g1 |> g by A22, A60, A54, A61, A62; :: thesis:
for g1 being morphism of CategoryStr(# car,comp #) st g1 |> g holds
g1 (*) g = g1

let g1 be morphism of CategoryStr(# car,comp #); :: thesis:
assume g1 |> g ; :: thesis:
then consider f11, f12, f13 being morphism of C1, f21, f22, f23 being morphism of C2 such that
A63: ( g1 = [f11,f21] & g = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g1 (*) g = [f13,f23] ) by A13;
A64: ( d11 = f12 & d22 = f22 ) by A61, A62, A63, XTUPLE_0:1;
( f13 = f11 & f23 = f21 ) by A64, A63, CAT_6:def 5, A61, A62, CAT_6:def 14;
hence g1 (*) g = g1 by A63; :: thesis:

end;

hence g is right_identity by CAT_6:def 5; :: thesis:

end;

for g1, g2, g3 being morphism of CategoryStr(# car,comp #) st g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 holds
g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3

let g1, g2, g3 be morphism of CategoryStr(# car,comp #); :: thesis:
assume g1 |> g2 ; :: thesis:
then consider f011, f012, f013 being morphism of C1, f021, f022, f023 being morphism of C2 such that
A65: ( g1 = [f011,f021] & g2 = [f012,f022] & F1 . f011 = F2 . f021 & F1 . f012 = F2 . f022 & f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 & g1 (*) g2 = [f013,f023] ) by A13;
assume g2 |> g3 ; :: thesis:
then consider f111, f112, f113 being morphism of C1, f121, f122, f123 being morphism of C2 such that
A66: ( g2 = [f111,f121] & g3 = [f112,f122] & F1 . f111 = F2 . f121 & F1 . f112 = F2 . f122 & f111 |> f112 & f121 |> f122 & f113 = f111 (*) f112 & f123 = f121 (*) f122 & g2 (*) g3 = [f113,f123] ) by A13;
assume g1 (*) g2 |> g3 ; :: thesis:
then consider f211, f212, f213 being morphism of C1, f221, f222, f223 being morphism of C2 such that
A67: ( g1 (*) g2 = [f211,f221] & g3 = [f212,f222] & F1 . f211 = F2 . f221 & F1 . f212 = F2 . f222 & f211 |> f212 & f221 |> f222 & f213 = f211 (*) f212 & f223 = f221 (*) f222 & (g1 (*) g2) (*) g3 = [f213,f223] ) by A13;
assume g1 |> g2 (*) g3 ; :: thesis:
then consider f311, f312, f313 being morphism of C1, f321, f322, f323 being morphism of C2 such that
A68: ( g1 = [f311,f321] & g2 (*) g3 = [f312,f322] & F1 . f311 = F2 . f321 & F1 . f312 = F2 . f322 & f311 |> f312 & f321 |> f322 & f313 = f311 (*) f312 & f323 = f321 (*) f322 & g1 (*) (g2 (*) g3) = [f313,f323] ) by A13;
A69: ( f113 = f312 & f123 = f322 ) by A66, A68, XTUPLE_0:1;
A70: ( f013 = f211 & f023 = f221 ) by A65, A67, XTUPLE_0:1;
A71: ( f011 = f311 & f021 = f321 ) by A65, A68, XTUPLE_0:1;
A72: ( f012 = f111 & f022 = f121 ) by A65, A66, XTUPLE_0:1;
A73: ( f112 = f212 & f122 = f222 ) by A66, A67, XTUPLE_0:1;
A74: f313 = f213 by A67, A65, A66, A68, A69, A70, A71, A72, A73, CAT_6:def 10;
thus g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 by A68, A67, A74, A65, A66, A69, A70, A71, A72, A73, CAT_6:def 10; :: thesis:

end;

then reconsider D = CategoryStr(# car,comp #) as strict category by A53, A52, A34, A33, CAT_6:def 10, CAT_6:def 11, CAT_6:def 12, CAT_6:def 7, CAT_6:def 9;
A75: for x being object holds
( x in comp iff x in { [[f1,f2],f3] where f1, f2, f3 is morphism of D : ( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } )

let x be object ; :: thesis:

hereby :: thesis:

assume x in comp ; :: thesis:
then consider x1, x2, x3 being Element of car such that
A76: ( x = [[x1,x2],x3] & x1 in car & x2 in car & x3 in car & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] & x3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) ;
reconsider f1 = x1, f2 = x2, f3 = x3 as morphism of D by CAT_6:def 1;
( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) by A76;
hence x in { [[f1,f2],f3] where f1, f2, f3 is morphism of D : ( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } by A76; :: thesis:

end;

assume x in { [[f1,f2],f3] where f1, f2, f3 is morphism of D : ( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } ; :: thesis:
then consider f1, f2, f3 being morphism of D such that
A77: ( x = [[f1,f2],f3] & f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) ;
reconsider x1 = f1, x2 = f2, x3 = f3 as Element of car by A77;
thus x in comp by A77; :: thesis:

end;

ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( P1 is covariant & P2 is covariant & F1 (*) P1 = F2 (*) P2 & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) ) ) )

suppose A78: D is empty ; :: thesis:

then reconsider D0 = D as empty category ;
reconsider P1 = the covariant Functor of D0,C1 as Functor of D,C1 ;
reconsider P2 = the covariant Functor of D0,C2 as Functor of D,C2 ;
take P1 ; :: thesis:
take P2 ; :: thesis:
thus ( P1 is covariant & P2 is covariant & F1 (*) P1 = F2 (*) P2 ) ; :: thesis:
let D1 be category; :: thesis:
let G1 be Functor of D1,C1; :: thesis:
let G2 be Functor of D1,C2; :: thesis:
assume A79: G1 is covariant ; :: thesis:
assume A80: G2 is covariant ; :: thesis:
assume A81: F1 (*) G1 = F2 (*) G2 ; :: thesis:
D1 is empty

assume A82: not D1 is empty ; :: thesis:
then consider x being object such that
A83: x in the carrier of D1 by XBOOLE_0:def 1;
reconsider d = x as morphism of D1 by A83, CAT_6:def 1;
set f1 = G1 . d;
set f2 = G2 . d;
A84: ( not C1 is empty & not C2 is empty ) by A82, A79, A80, CAT_6:31;
A85: ( x in dom G1 & x in dom G2 ) by A84, A83, FUNCT_2:def 1;
A86: G1 . d = G1 . x by A82, CAT_6:def 21;
A87: G2 . d = G2 . x by A82, CAT_6:def 21;
A88: F1 . (G1 . d) = F1 . (G1 . x) by A86, A84, CAT_6:def 21
.= (G1 * F1) . x by A85, FUNCT_1:13
.= (F2 (*) G2) . x by A81, A1, A79, CAT_6:def 27
.= (G2 * F2) . x by A1, A80, CAT_6:def 27
.= F2 . (G2 . x) by A85, FUNCT_1:13
.= F2 . (G2 . d) by A87, A84, CAT_6:def 21 ;
( G1 . d in the carrier of C1 & G2 . d in the carrier of C2 ) by A84, Th1;
then [(G1 . d),(G2 . d)] in the carrier of D by A88;
hence contradiction by A78; :: thesis:

end;

then reconsider D01 = D1 as empty category ;
reconsider H = the covariant Functor of D01,D as Functor of D1,D ;
take H ; :: thesis:
thus ( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 ) ; :: thesis:
let H1 be Functor of D1,D; :: thesis:
assume ( H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 ) ; :: thesis:
thus H = H1 ; :: thesis:

end;

suppose A89: not D is empty ; :: thesis:

deffunc H₁( object ) -> object = $1 `1 ;
A90: for x being object st x in the carrier of D holds
H₁(x) in the carrier of C1

let x be object ; :: thesis:
assume x in the carrier of D ; :: thesis:
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A91: ( x = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) ;
thus H₁(x) in the carrier of C1 by A91; :: thesis:

end;

consider P1 being Function of the carrier of D, the carrier of C1 such that
A92: for x being object st x in the carrier of D holds
P1 . x = H₁(x) from FUNCT_2:sch 2(A90);
reconsider P1 = P1 as Functor of D,C1 ;
deffunc H₂( object ) -> object = $1 `2 ;
A93: for x being object st x in the carrier of D holds
H₂(x) in the carrier of C2

let x be object ; :: thesis:
assume x in the carrier of D ; :: thesis:
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A94: ( x = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) ;
thus H₂(x) in the carrier of C2 by A94; :: thesis:

end;

consider P2 being Function of the carrier of D, the carrier of C2 such that
A95: for x being object st x in the carrier of D holds
P2 . x = H₂(x) from FUNCT_2:sch 2(A93);
reconsider P2 = P2 as Functor of D,C2 ;
take P1 ; :: thesis:
take P2 ; :: thesis:
A96: for g being morphism of D st g is identity holds
ex f1 being morphism of C1 ex f2 being morphism of C2 st
( g = [f1,f2] & f1 is identity & f2 is identity )

let g be morphism of D; :: thesis:
assume A97: g is identity ; :: thesis:
g in the carrier of D by A89, Th1;
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A98: ( g = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) ;
take f1 ; :: thesis:
take f2 ; :: thesis:
A99: not C1 is empty by A98;
then consider d1 being morphism of C1 such that
A100: ( dom f1 = d1 & f1 |> d1 & d1 is identity ) by CAT_6:def 18;
A101: not C2 is empty by A98;
then consider d2 being morphism of C2 such that
A102: ( dom f2 = d2 & f2 |> d2 & d2 is identity ) by CAT_6:def 18;
set g1 = [d1,d2];
A103: not C is empty by A1, A99, CAT_6:31;
A104: ( d1 in the carrier of C1 & d2 in the carrier of C2 ) by A99, A101, Th1;
A105: F1 . d1 = F1 . (dom f1) by A99, A100, CAT_6:def 21
.= dom (F2 . f2) by A98, A1, A99, A103, CAT_6:32
.= F2 . (dom f2) by A1, A101, A103, CAT_6:32
.= F2 . d2 by A101, A102, CAT_6:def 21 ;
then [d1,d2] in the carrier of D by A104;
then reconsider g1 = [d1,d2] as morphism of D by CAT_6:def 1;
A106: g |> g1 by A22, A98, A105, A100, A102;
thus g = [f1,f2] by A98; :: thesis:
consider f11, f12, f13 being morphism of C1, f21, f22, f23 being morphism of C2 such that
A107: ( g = [f11,f21] & g1 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g (*) g1 = [f13,f23] ) by A13, A22, A98, A105, A100, A102;
A108: ( f11 = f1 & f21 = f2 & f12 = d1 & f22 = d2 ) by A98, A107, XTUPLE_0:1;
( f1 = f1 (*) d1 & f2 = f2 (*) d2 ) by A100, A102, CAT_6:def 5, CAT_6:def 14;
then g = g1 by A106, A97, CAT_6:def 14, CAT_6:def 4, A108, A107;
hence ( f1 is identity & f2 is identity ) by A100, A102, A98, XTUPLE_0:1; :: thesis:

end;

for g being morphism of D st g is identity holds
( P1 . g is identity & P2 . g is identity )

let g be morphism of D; :: thesis:
assume g is identity ; :: thesis:
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A109: ( g = [f1,f2] & f1 is identity & f2 is identity ) by A96;
reconsider x = g as object ;
P1 . g = P1 . x by CAT_6:def 21, A89
.= H₁(x) by A92, A89, Th1
.= f1 by A109 ;
hence P1 . g is identity by A109; :: thesis:
P2 . g = P2 . x by CAT_6:def 21, A89
.= H₂(x) by A95, A89, Th1
.= f2 by A109 ;
hence P2 . g is identity by A109; :: thesis:

end;

then ( ( for g being morphism of D st g is identity holds
P1 . g is identity ) & ( for g being morphism of D st g is identity holds
P2 . g is identity ) ) ;
then A110: ( P1 is identity-preserving & P2 is identity-preserving ) by CAT_6:def 22;
for g1, g2 being morphism of D st g1 |> g2 holds
( P1 . g1 |> P1 . g2 & P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) & P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) )

let g1, g2 be morphism of D; :: thesis:
assume g1 |> g2 ; :: thesis:
then consider f11, f12, f13 being morphism of C1, f21, f22, f23 being morphism of C2 such that
A111: ( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g1 (*) g2 = [f13,f23] ) by A13;
reconsider x1 = g1, x2 = g2, x12 = g1 (*) g2 as object ;
A112: P1 . g1 = P1 . x1 by CAT_6:def 21, A89
.= H₁(x1) by A92, A89, Th1
.= f11 by A111 ;
A113: P1 . g2 = P1 . x2 by CAT_6:def 21, A89
.= H₁(x2) by A92, A89, Th1
.= f12 by A111 ;
A114: P1 . (g1 (*) g2) = P1 . x12 by CAT_6:def 21, A89
.= H₁(x12) by A92, A89, Th1
.= f13 by A111 ;
thus P1 . g1 |> P1 . g2 by A112, A113, A111; :: thesis:
thus P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) by A112, A113, A114, A111; :: thesis:
A115: P2 . g1 = P2 . x1 by CAT_6:def 21, A89
.= H₂(x1) by A95, A89, Th1
.= f21 by A111 ;
A116: P2 . g2 = P2 . x2 by CAT_6:def 21, A89
.= H₂(x2) by A95, A89, Th1
.= f22 by A111 ;
A117: P2 . (g1 (*) g2) = P2 . x12 by CAT_6:def 21, A89
.= H₂(x12) by A95, A89, Th1
.= f23 by A111 ;
thus P2 . g1 |> P2 . g2 by A115, A116, A111; :: thesis:
thus P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) by A115, A116, A117, A111; :: thesis:

end;

then ( ( for g1, g2 being morphism of D st g1 |> g2 holds
( P1 . g1 |> P1 . g2 & P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) ) ) & ( for g1, g2 being morphism of D st g1 |> g2 holds
( P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) ) ) ) ;
hence A118: ( P1 is covariant & P2 is covariant ) by A110, CAT_6:def 23, CAT_6:def 25; :: thesis:
for x being object st x in the carrier of D holds
(F1 (*) P1) . x = (F2 (*) P2) . x

let x be object ; :: thesis:
assume A119: x in the carrier of D ; :: thesis:
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A120: ( x = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) ;
reconsider g = x as morphism of D by A119, CAT_6:def 1;
A121: P1 . g = P1 . x by CAT_6:def 21, A89
.= H₁(x) by A92, A119
.= f1 by A120 ;
A122: P2 . g = P2 . x by CAT_6:def 21, A89
.= H₂(x) by A95, A119
.= f2 by A120 ;
thus (F1 (*) P1) . x = (F1 (*) P1) . g by A89, CAT_6:def 21
.= F1 . f1 by A121, A89, A1, A118, CAT_6:34
.= (F2 (*) P2) . g by A89, A1, A118, CAT_6:34, A122, A120
.= (F2 (*) P2) . x by A89, CAT_6:def 21 ; :: thesis:

end;

hence F1 (*) P1 = F2 (*) P2 by FUNCT_2:12; :: thesis:
let D1 be category; :: thesis:
let G1 be Functor of D1,C1; :: thesis:
let G2 be Functor of D1,C2; :: thesis:
assume A123: G1 is covariant ; :: thesis:
assume A124: G2 is covariant ; :: thesis:
assume A125: F1 (*) G1 = F2 (*) G2 ; :: thesis:
deffunc H₃( object ) -> object = [(G1 . $1),(G2 . $1)];
A126: for x being object st x in the carrier of D1 holds
H₃(x) in the carrier of D

let x be object ; :: thesis:
assume A127: x in the carrier of D1 ; :: thesis:
then A128: not D1 is empty ;
reconsider d = x as morphism of D1 by A127, CAT_6:def 1;
A129: ( not C1 is empty & not C2 is empty ) by A89, A118, CAT_6:31;
A130: ( G1 . d in the carrier of C1 & G2 . d in the carrier of C2 ) by A129, Th1;
A131: ( G1 . d = G1 . x & G2 . d = G2 . x ) by A128, CAT_6:def 21;
F1 . (G1 . d) = (F1 (*) G1) . d by A123, A128, A1, CAT_6:34
.= F2 . (G2 . d) by A124, A125, A128, A1, CAT_6:34 ;
hence H₃(x) in the carrier of D by A130, A131; :: thesis:

end;

consider H being Function of the carrier of D1, the carrier of D such that
A132: for x being object st x in the carrier of D1 holds
H . x = H₃(x) from FUNCT_2:sch 2(A126);
reconsider H = H as Functor of D1,D ;
take H ; :: thesis:
for d being morphism of D1 st d is identity holds
H . d is identity

let d be morphism of D1; :: thesis:
assume A133: d is identity ; :: thesis:

suppose D1 is empty ; :: thesis:

then H . d = the Object of D by CAT_6:def 21;
hence H . d is identity by A89, CAT_6:22; :: thesis:

end;

suppose A134: not D1 is empty ; :: thesis:

for g1 being morphism of D st H . d |> g1 holds
(H . d) (*) g1 = g1

let g1 be morphism of D; :: thesis:
assume H . d |> g1 ; :: thesis:
then consider d1, f1, f13 being morphism of C1, d2, f2, f23 being morphism of C2 such that
A135: ( H . d = [d1,d2] & g1 = [f1,f2] & F1 . d1 = F2 . d2 & F1 . f1 = F2 . f2 & d1 |> f1 & d2 |> f2 & f13 = d1 (*) f1 & f23 = d2 (*) f2 & (H . d) (*) g1 = [f13,f23] ) by A13;
reconsider x = d as object ;
A136: ( G1 . x = G1 . d & G2 . x = G2 . d ) by A134, CAT_6:def 21;
H . d = H . x by A134, CAT_6:def 21
.= [(G1 . d),(G2 . d)] by A136, A134, Th1, A132 ;
then ( d1 = G1 . d & d2 = G2 . d ) by A135, XTUPLE_0:1;
then ( d1 is identity & d2 is identity ) by A133, CAT_6:def 22, A123, A124, CAT_6:def 25;
then ( d1 (*) f1 = f1 & d2 (*) f2 = f2 ) by A135, CAT_6:def 14, CAT_6:def 4;
hence (H . d) (*) g1 = g1 by A135; :: thesis:

end;

then A137: H . d is left_identity by CAT_6:def 4;
for g1 being morphism of D st g1 |> H . d holds
g1 (*) (H . d) = g1

let g1 be morphism of D; :: thesis:
assume g1 |> H . d ; :: thesis:
then consider f1, d1, f13 being morphism of C1, f2, d2, f23 being morphism of C2 such that
A138: ( g1 = [f1,f2] & H . d = [d1,d2] & F1 . f1 = F2 . f2 & F1 . d1 = F2 . d2 & f1 |> d1 & f2 |> d2 & f13 = f1 (*) d1 & f23 = f2 (*) d2 & g1 (*) (H . d) = [f13,f23] ) by A13;
reconsider x = d as object ;
A139: ( G1 . x = G1 . d & G2 . x = G2 . d ) by A134, CAT_6:def 21;
H . d = H . x by A134, CAT_6:def 21
.= [(G1 . d),(G2 . d)] by A139, A134, Th1, A132 ;
then ( d1 = G1 . d & d2 = G2 . d ) by A138, XTUPLE_0:1;
then ( d1 is identity & d2 is identity ) by A133, CAT_6:def 22, A123, A124, CAT_6:def 25;
then ( f1 (*) d1 = f1 & f2 (*) d2 = f2 ) by A138, CAT_6:def 14, CAT_6:def 5;
hence g1 (*) (H . d) = g1 by A138; :: thesis:

end;

hence H . d is identity by A137, CAT_6:def 5, CAT_6:def 14; :: thesis:

end;

end;

end;

then A140: H is identity-preserving by CAT_6:def 22;
for d1, d2 being morphism of D1 st d1 |> d2 holds
( H . d1 |> H . d2 & H . (d1 (*) d2) = (H . d1) (*) (H . d2) )

let d1, d2 be morphism of D1; :: thesis:
assume A141: d1 |> d2 ; :: thesis:
then A142: not D1 is empty by CAT_6:1;
reconsider x1 = d1, x2 = d2 as object ;
A143: ( G1 . x1 = G1 . d1 & G2 . x1 = G2 . d1 ) by A142, CAT_6:def 21;
A144: ( G1 . x2 = G1 . d2 & G2 . x2 = G2 . d2 ) by A142, CAT_6:def 21;
A145: ( G1 is multiplicative & G2 is multiplicative ) by A123, A124, CAT_6:def 25;
A146: d1 in the carrier of D1 by A141, Th1, CAT_6:1;
A147: H . d1 = H . x1 by A142, CAT_6:def 21
.= [(G1 . d1),(G2 . d1)] by A143, A146, A132 ;
H . d1 in the carrier of D by A89, Th1;
then consider f11 being morphism of C1, f21 being morphism of C2 such that
A148: ( H . d1 = [f11,f21] & f11 in the carrier of C1 & f21 in the carrier of C2 & F1 . f11 = F2 . f21 ) ;
A149: d2 in the carrier of D1 by A141, Th1, CAT_6:1;
A150: H . d2 = H . x2 by A142, CAT_6:def 21
.= [(G1 . d2),(G2 . d2)] by A144, A149, A132 ;
H . d2 in the carrier of D by A89, Th1;
then consider f12 being morphism of C1, f22 being morphism of C2 such that
A151: ( H . d2 = [f12,f22] & f12 in the carrier of C1 & f22 in the carrier of C2 & F1 . f12 = F2 . f22 ) ;
A152: ( f11 = G1 . d1 & f21 = G2 . d1 ) by A148, A147, XTUPLE_0:1;
A153: ( f12 = G1 . d2 & f22 = G2 . d2 ) by A151, A150, XTUPLE_0:1;
A154: ( G1 . d1 |> G1 . d2 & G1 . (d1 (*) d2) = (G1 . d1) (*) (G1 . d2) ) by A141, A145, CAT_6:def 23;
A155: ( G2 . d1 |> G2 . d2 & G2 . (d1 (*) d2) = (G2 . d1) (*) (G2 . d2) ) by A141, A145, CAT_6:def 23;
thus H . d1 |> H . d2 by A22, A152, A153, A154, A155, A148, A151; :: thesis:
consider f011, f012, f013 being morphism of C1, f021, f022, f023 being morphism of C2 such that
A156: ( H . d1 = [f011,f021] & H . d2 = [f012,f022] & F1 . f011 = F2 . f021 & F1 . f012 = F2 . f022 & f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 & (H . d1) (*) (H . d2) = [f013,f023] ) by A13, A22, A152, A153, A154, A155, A148, A151;
A157: ( f011 = G1 . d1 & f021 = G2 . d1 & f012 = G1 . d2 & f022 = G2 . d2 ) by A156, A150, A147, XTUPLE_0:1;
reconsider x12 = d1 (*) d2 as object ;
A158: ( G1 . x12 = G1 . (d1 (*) d2) & G2 . x12 = G2 . (d1 (*) d2) ) by A142, CAT_6:def 21;
thus H . (d1 (*) d2) = H . x12 by A142, CAT_6:def 21
.= (H . d1) (*) (H . d2) by A154, A155, A156, A157, A158, A142, Th1, A132 ; :: thesis:

end;

hence A159: H is covariant by A140, CAT_6:def 23, CAT_6:def 25; :: thesis:
for x being object st x in the carrier of D1 holds
(P1 (*) H) . x = G1 . x

let x be object ; :: thesis:
assume A160: x in the carrier of D1 ; :: thesis:
then A161: not D1 is empty ;
reconsider d = x as morphism of D1 by A160, CAT_6:def 1;
A162: H . d = H . x by A161, CAT_6:def 21
.= [(G1 . x),(G2 . x)] by A160, A132 ;
reconsider x1 = H . d as object ;
thus (P1 (*) H) . x = (P1 (*) H) . d by A161, CAT_6:def 21
.= P1 . (H . d) by A161, A118, A159, CAT_6:34
.= P1 . x1 by A89, CAT_6:def 21
.= H₁([(G1 . x),(G2 . x)]) by A92, A89, Th1, A162
.= G1 . x ; :: thesis:

end;

hence P1 (*) H = G1 by FUNCT_2:12; :: thesis:
for x being object st x in the carrier of D1 holds
(P2 (*) H) . x = G2 . x

let x be object ; :: thesis:
assume A163: x in the carrier of D1 ; :: thesis:
then A164: not D1 is empty ;
reconsider d = x as morphism of D1 by A163, CAT_6:def 1;
A165: H . d = H . x by A164, CAT_6:def 21
.= [(G1 . x),(G2 . x)] by A163, A132 ;
reconsider x2 = H . d as object ;
thus (P2 (*) H) . x = (P2 (*) H) . d by A164, CAT_6:def 21
.= P2 . (H . d) by A164, A118, A159, CAT_6:34
.= P2 . x2 by A89, CAT_6:def 21
.= H₂([(G1 . x),(G2 . x)]) by A165, A95, A89, Th1
.= G2 . x ; :: thesis:

end;

hence P2 (*) H = G2 by FUNCT_2:12; :: thesis:
let H1 be Functor of D1,D; :: thesis:
assume A166: H1 is covariant ; :: thesis:
assume A167: P1 (*) H1 = G1 ; :: thesis:
assume A168: P2 (*) H1 = G2 ; :: thesis:
for x being object st x in the carrier of D1 holds
H . x = H1 . x

let x be object ; :: thesis:
assume A169: x in the carrier of D1 ; :: thesis:
then A170: not D1 is empty ;
reconsider d = x as morphism of D1 by A169, CAT_6:def 1;
A171: ( G1 . x = G1 . d & G2 . x = G2 . d ) by A170, CAT_6:def 21;
H1 . d in the carrier of D by A89, Th1;
then consider f1 being morphism of C1, f2 being morphism of C2 such that
A172: ( H1 . d = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) ;
reconsider x1 = H1 . d as object ;
A173: G1 . d = P1 . (H1 . d) by A167, A170, A166, A118, CAT_6:34
.= P1 . x1 by A89, CAT_6:def 21
.= H₁([f1,f2]) by A172, A92, A89, Th1
.= f1 ;
A174: G2 . d = P2 . (H1 . d) by A168, A170, A166, A118, CAT_6:34
.= P2 . x1 by A89, CAT_6:def 21
.= H₂([f1,f2]) by A172, A95, A89, Th1
.= f2 ;
thus H . x = H1 . d by A173, A174, A172, A171, A169, A132
.= H1 . x by A170, CAT_6:def 21 ; :: thesis:

end;

hence H = H1 by FUNCT_2:12; :: thesis:

end;

end;

end;

then consider P1 being Functor of D,C1, P2 being Functor of D,C2 such that
A175: ( P1 is covariant & P2 is covariant & F1 (*) P1 = F2 (*) P2 & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) ) ) ) ;
take D ; :: thesis:
take P1 ; :: thesis:
take P2 ; :: thesis:
thus ( the carrier of D = { [f1,f2] where f1 is morphism of C1, f2 is morphism of C2 : ( f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) } & the composition of D = { [[f1,f2],f3] where f1, f2, f3 is morphism of D : ( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1
for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds
( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 ) by A75, A175, A1, Def20, TARSKI:2; :: thesis: