let C, C1, C2 be category; :: thesis: for F1 being Functor of C1,C

for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

let F2 be Functor of C2,C; :: thesis: ( F1 is covariant & F2 is covariant implies ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 ) )

assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

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:]

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

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] )

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

( g1 (*) g2 |> g iff g2 |> g )

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

( g |> g1 (*) g2 iff g |> g1 )

ex g being morphism of CategoryStr(# car,comp #) st

( g |> g1 & g is left_identity )

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 )

g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3

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 ) ) ) } )

( 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 ) ) ) )

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: ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

take P1 ; :: thesis: ex P2 being Functor of D,C2 st

( 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 )

take P2 ; :: thesis: ( 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 )

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: verum

for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds

ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

let F2 be Functor of C2,C; :: thesis: ( F1 is covariant & F2 is covariant implies ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 ) )

assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

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:]

proof

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
let x be object ; :: thesis: ( 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 ) ) ) } implies x in [:[:car,car:],car:] )

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: x in [:[:car,car:],car:]

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: verum

end;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 ) ) ) } implies x in [:[:car,car:],car:] )

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: x in [:[:car,car:],car:]

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: verum

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

proof

then reconsider comp = comp as PartFunc of [:car,car:],car by FUNCT_1:def 1;
let x, y1, y2 be object ; :: thesis: ( [x,y1] in comp & [x,y2] in comp implies y1 = y2 )

assume [x,y1] in comp ; :: thesis: ( not [x,y2] in comp or y1 = y2 )

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: y1 = y2

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: verum

end;assume [x,y1] in comp ; :: thesis: ( not [x,y2] in comp or y1 = y2 )

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: y1 = y2

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: verum

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] )

proof

A21:
( F1 is multiplicative & F2 is multiplicative )
by A1, CAT_6:def 25;
let g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis: ( g1 |> g2 implies 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] ) )

assume A14: g1 |> g2 ; :: thesis: 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] )

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: ex 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] )

take f12 ; :: thesis: ex 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] )

take f13 ; :: thesis: 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] )

take f21 ; :: thesis: ex 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] )

take f22 ; :: thesis: ex 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] )

take f23 ; :: thesis: ( 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] )

thus ( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 ) by A15, A16; :: thesis: ( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g1 (*) g2 = [f13,f23] )

thus ( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) by A20, A18, A19, A15, A16; :: thesis: g1 (*) g2 = [f13,f23]

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: verum

end;( 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] ) )

assume A14: g1 |> g2 ; :: thesis: 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] )

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: ex 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] )

take f12 ; :: thesis: ex 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] )

take f13 ; :: thesis: 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] )

take f21 ; :: thesis: ex 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] )

take f22 ; :: thesis: ex 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] )

take f23 ; :: thesis: ( 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] )

thus ( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 ) by A15, A16; :: thesis: ( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 & g1 (*) g2 = [f13,f23] )

thus ( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) by A20, A18, A19, A15, A16; :: thesis: g1 (*) g2 = [f13,f23]

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: verum

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

proof

for g, g1, g2 being morphism of CategoryStr(# car,comp #) st g1 |> g2 holds
let g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis: ( 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 ) implies g1 |> g2 )

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: g1 |> g2

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 )

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: verum

end;( g1 = [f11,f21] & g2 = [f12,f22] & F1 . f11 = F2 . f21 & F1 . f12 = F2 . f22 & f11 |> f12 & f21 |> f22 ) implies g1 |> g2 )

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: g1 |> g2

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 )

proof

then
[[x1,x2],x3] in the composition of CategoryStr(# car,comp #)
by A26;
let f011, f012, f013 be morphism of C1; :: thesis: 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 f021, f022, f023 be morphism of C2; :: thesis: ( x1 = [f011,f021] & x2 = [f012,f022] & x3 = [f013,f023] implies ( f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 ) )

assume ( x1 = [f011,f021] & x2 = [f012,f022] & x3 = [f013,f023] ) ; :: thesis: ( f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 )

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: verum

end;( f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 )

let f021, f022, f023 be morphism of C2; :: thesis: ( x1 = [f011,f021] & x2 = [f012,f022] & x3 = [f013,f023] implies ( f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 ) )

assume ( x1 = [f011,f021] & x2 = [f012,f022] & x3 = [f013,f023] ) ; :: thesis: ( f011 |> f012 & f021 |> f022 & f013 = f011 (*) f012 & f023 = f021 (*) f022 )

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: verum

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: verum

( g1 (*) g2 |> g iff g2 |> g )

proof

then A33:
CategoryStr(# car,comp #) is left_composable
by CAT_6:def 8;
let g, g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis: ( g1 |> g2 implies ( g1 (*) g2 |> g iff g2 |> g ) )

assume g1 |> g2 ; :: thesis: ( g1 (*) g2 |> g iff g2 |> g )

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;

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: verum

end;assume g1 |> g2 ; :: thesis: ( g1 (*) g2 |> g iff g2 |> g )

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: ( g2 |> g implies g1 (*) g2 |> g )

assume
g2 |> g
; :: thesis: g1 (*) g2 |> gassume
g1 (*) g2 |> g
; :: thesis: g2 |> g

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: verum

end;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: verum

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: verum

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

( g |> g1 (*) g2 iff g |> g1 )

proof

for g1 being morphism of CategoryStr(# car,comp #) st g1 in the carrier of CategoryStr(# car,comp #) holds
let g, g1, g2 be morphism of CategoryStr(# car,comp #); :: thesis: ( g1 |> g2 implies ( g |> g1 (*) g2 iff g |> g1 ) )

assume g1 |> g2 ; :: thesis: ( g |> g1 (*) g2 iff g |> g1 )

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;

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: verum

end;assume g1 |> g2 ; :: thesis: ( g |> g1 (*) g2 iff g |> g1 )

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: ( g |> g1 implies g |> g1 (*) g2 )

assume
g |> g1
; :: thesis: g |> g1 (*) g2assume
g |> g1 (*) g2
; :: thesis: g |> g1

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: verum

end;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: verum

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: verum

ex g being morphism of CategoryStr(# car,comp #) st

( g |> g1 & g is left_identity )

proof

then A52:
CategoryStr(# car,comp #) is with_left_identities
by CAT_6:def 6;
let g1 be morphism of CategoryStr(# car,comp #); :: thesis: ( g1 in the carrier of CategoryStr(# car,comp #) implies ex g being morphism of CategoryStr(# car,comp #) st

( g |> g1 & g is left_identity ) )

assume g1 in the carrier of CategoryStr(# car,comp #) ; :: thesis: ex g being morphism of CategoryStr(# car,comp #) st

( g |> g1 & g is left_identity )

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: ( g |> g1 & g is left_identity )

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: g is left_identity

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

g (*) g1 = g1

end;( g |> g1 & g is left_identity ) )

assume g1 in the carrier of CategoryStr(# car,comp #) ; :: thesis: ex g being morphism of CategoryStr(# car,comp #) st

( g |> g1 & g is left_identity )

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: ( g |> g1 & g is left_identity )

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: g is left_identity

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

g (*) g1 = g1

proof

hence
g is left_identity
by CAT_6:def 4; :: thesis: verum
let g1 be morphism of CategoryStr(# car,comp #); :: thesis: ( g |> g1 implies g (*) g1 = g1 )

assume g |> g1 ; :: thesis: g (*) g1 = g1

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: verum

end;assume g |> g1 ; :: thesis: g (*) g1 = g1

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: verum

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 )

proof

for g1, g2, g3 being morphism of CategoryStr(# car,comp #) st g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 holds
let g1 be morphism of CategoryStr(# car,comp #); :: thesis: ( g1 in the carrier of CategoryStr(# car,comp #) implies ex g being morphism of CategoryStr(# car,comp #) st

( g1 |> g & g is right_identity ) )

assume g1 in the carrier of CategoryStr(# car,comp #) ; :: thesis: ex g being morphism of CategoryStr(# car,comp #) st

( g1 |> g & g is right_identity )

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: ( g1 |> g & g is right_identity )

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: g is right_identity

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

g1 (*) g = g1

end;( g1 |> g & g is right_identity ) )

assume g1 in the carrier of CategoryStr(# car,comp #) ; :: thesis: ex g being morphism of CategoryStr(# car,comp #) st

( g1 |> g & g is right_identity )

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: ( g1 |> g & g is right_identity )

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: g is right_identity

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

g1 (*) g = g1

proof

hence
g is right_identity
by CAT_6:def 5; :: thesis: verum
let g1 be morphism of CategoryStr(# car,comp #); :: thesis: ( g1 |> g implies g1 (*) g = g1 )

assume g1 |> g ; :: thesis: g1 (*) g = g1

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: verum

end;assume g1 |> g ; :: thesis: g1 (*) g = g1

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: verum

g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3

proof

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;
let g1, g2, g3 be morphism of CategoryStr(# car,comp #); :: thesis: ( g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 implies g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )

assume g1 |> g2 ; :: thesis: ( not g2 |> g3 or not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )

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: ( not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )

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: ( not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )

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: g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3

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: verum

end;assume g1 |> g2 ; :: thesis: ( not g2 |> g3 or not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )

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: ( not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )

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: ( not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )

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: g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3

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: verum

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 ) ) ) } )

proof

ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
let x be object ; :: thesis: ( 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 ) ) ) } )

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: x in comp

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: verum

end;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 ) ) ) } )

hereby :: thesis: ( 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 ) ) ) } implies x in comp )

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 C1for 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 ) ) ) } implies x in comp )

assume
x in comp
; :: thesis: 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 ) ) ) }

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: verum

end;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 ) ) ) }

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: verum

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: x in comp

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: verum

( 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 ) ) ) )

proof
end;

then consider P1 being Functor of D,C1, P2 being Functor of D,C2 such that per cases
( D is empty or not D is empty )
;

end;

suppose A78:
D is empty
; :: thesis: 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 ) ) ) )

( 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 ) ) ) )

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: 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 ) ) ) )

take P2 ; :: thesis: ( 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 ) ) ) )

thus ( P1 is covariant & P2 is covariant & F1 (*) P1 = F2 (*) P2 ) ; :: thesis: 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 ) )

let D1 be category; :: thesis: 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 ) )

let G1 be Functor of D1,C1; :: thesis: 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 ) )

let G2 be Functor of D1,C2; :: thesis: ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 implies 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 ) ) )

assume A79: G1 is covariant ; :: thesis: ( not G2 is covariant or not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A80: G2 is covariant ; :: thesis: ( not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A81: F1 (*) G1 = F2 (*) G2 ; :: thesis: 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 ) )

D1 is empty

reconsider H = the covariant Functor of D01,D as Functor of D1,D ;

take H ; :: thesis: ( 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 ) )

thus ( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 ) ; :: thesis: for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1

let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 implies H = H1 )

assume ( H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 ) ; :: thesis: H = H1

thus H = H1 ; :: thesis: verum

end;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: 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 ) ) ) )

take P2 ; :: thesis: ( 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 ) ) ) )

thus ( P1 is covariant & P2 is covariant & F1 (*) P1 = F2 (*) P2 ) ; :: thesis: 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 ) )

let D1 be category; :: thesis: 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 ) )

let G1 be Functor of D1,C1; :: thesis: 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 ) )

let G2 be Functor of D1,C2; :: thesis: ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 implies 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 ) ) )

assume A79: G1 is covariant ; :: thesis: ( not G2 is covariant or not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A80: G2 is covariant ; :: thesis: ( not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A81: F1 (*) G1 = F2 (*) G2 ; :: thesis: 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 ) )

D1 is empty

proof

then reconsider D01 = D1 as empty category ;
assume A82:
not D1 is empty
; :: thesis: contradiction

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: verum

end;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: verum

reconsider H = the covariant Functor of D01,D as Functor of D1,D ;

take H ; :: thesis: ( 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 ) )

thus ( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 ) ; :: thesis: for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1

let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 implies H = H1 )

assume ( H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 ) ; :: thesis: H = H1

thus H = H1 ; :: thesis: verum

suppose A89:
not D is empty
; :: thesis: 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 ) ) ) )

( 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 ) ) ) )

deffunc H_{1}( object ) -> object = $1 `1 ;

A90: for x being object st x in the carrier of D holds

H_{1}(x) in the carrier of C1

A92: for x being object st x in the carrier of D holds

P1 . x = H_{1}(x)
from FUNCT_2:sch 2(A90);

reconsider P1 = P1 as Functor of D,C1 ;

deffunc H_{2}( object ) -> object = $1 `2 ;

A93: for x being object st x in the carrier of D holds

H_{2}(x) in the carrier of C2

A95: for x being object st x in the carrier of D holds

P2 . x = H_{2}(x)
from FUNCT_2:sch 2(A93);

reconsider P2 = P2 as Functor of D,C2 ;

take P1 ; :: thesis: 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 ) ) ) )

take P2 ; :: thesis: ( 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 ) ) ) )

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 )

( P1 . g is identity & P2 . g is identity )

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) )

( 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: ( 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 ) ) ) )

for x being object st x in the carrier of D holds

(F1 (*) P1) . x = (F2 (*) P2) . x

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 ) )

let D1 be category; :: thesis: 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 ) )

let G1 be Functor of D1,C1; :: thesis: 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 ) )

let G2 be Functor of D1,C2; :: thesis: ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 implies 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 ) ) )

assume A123: G1 is covariant ; :: thesis: ( not G2 is covariant or not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A124: G2 is covariant ; :: thesis: ( not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A125: F1 (*) G1 = F2 (*) G2 ; :: thesis: 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 ) )

deffunc H_{3}( object ) -> object = [(G1 . $1),(G2 . $1)];

A126: for x being object st x in the carrier of D1 holds

H_{3}(x) in the carrier of D

A132: for x being object st x in the carrier of D1 holds

H . x = H_{3}(x)
from FUNCT_2:sch 2(A126);

reconsider H = H as Functor of D1,D ;

take H ; :: thesis: ( 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 ) )

for d being morphism of D1 st d is identity holds

H . d is identity

for d1, d2 being morphism of D1 st d1 |> d2 holds

( H . d1 |> H . d2 & H . (d1 (*) d2) = (H . d1) (*) (H . d2) )

H = H1 ) )

for x being object st x in the carrier of D1 holds

(P1 (*) H) . x = G1 . x

H = H1 ) )

for x being object st x in the carrier of D1 holds

(P2 (*) H) . x = G2 . x

H = H1

let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 implies H = H1 )

assume A166: H1 is covariant ; :: thesis: ( not P1 (*) H1 = G1 or not P2 (*) H1 = G2 or H = H1 )

assume A167: P1 (*) H1 = G1 ; :: thesis: ( not P2 (*) H1 = G2 or H = H1 )

assume A168: P2 (*) H1 = G2 ; :: thesis: H = H1

for x being object st x in the carrier of D1 holds

H . x = H1 . x

end;A90: for x being object st x in the carrier of D holds

H

proof

consider P1 being Function of the carrier of D, the carrier of C1 such that
let x be object ; :: thesis: ( x in the carrier of D implies H_{1}(x) in the carrier of C1 )

assume x in the carrier of D ; :: thesis: H_{1}(x) in the carrier of C1

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_{1}(x) in the carrier of C1
by A91; :: thesis: verum

end;assume x in the carrier of D ; :: thesis: H

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

A92: for x being object st x in the carrier of D holds

P1 . x = H

reconsider P1 = P1 as Functor of D,C1 ;

deffunc H

A93: for x being object st x in the carrier of D holds

H

proof

consider P2 being Function of the carrier of D, the carrier of C2 such that
let x be object ; :: thesis: ( x in the carrier of D implies H_{2}(x) in the carrier of C2 )

assume x in the carrier of D ; :: thesis: H_{2}(x) in the carrier of C2

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_{2}(x) in the carrier of C2
by A94; :: thesis: verum

end;assume x in the carrier of D ; :: thesis: H

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

A95: for x being object st x in the carrier of D holds

P2 . x = H

reconsider P2 = P2 as Functor of D,C2 ;

take P1 ; :: thesis: 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 ) ) ) )

take P2 ; :: thesis: ( 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 ) ) ) )

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 )

proof

for g being morphism of D st g is identity holds
let g be morphism of D; :: thesis: ( g is identity implies ex f1 being morphism of C1 ex f2 being morphism of C2 st

( g = [f1,f2] & f1 is identity & f2 is identity ) )

assume A97: g is identity ; :: thesis: ex f1 being morphism of C1 ex f2 being morphism of C2 st

( g = [f1,f2] & f1 is identity & f2 is identity )

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: ex f2 being morphism of C2 st

( g = [f1,f2] & f1 is identity & f2 is identity )

take f2 ; :: thesis: ( g = [f1,f2] & f1 is identity & f2 is identity )

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: ( f1 is identity & f2 is identity )

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: verum

end;( g = [f1,f2] & f1 is identity & f2 is identity ) )

assume A97: g is identity ; :: thesis: ex f1 being morphism of C1 ex f2 being morphism of C2 st

( g = [f1,f2] & f1 is identity & f2 is identity )

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: ex f2 being morphism of C2 st

( g = [f1,f2] & f1 is identity & f2 is identity )

take f2 ; :: thesis: ( g = [f1,f2] & f1 is identity & f2 is identity )

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: ( f1 is identity & f2 is identity )

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: verum

( P1 . g is identity & P2 . g is identity )

proof

then
( ( for g being morphism of D st g is identity holds
let g be morphism of D; :: thesis: ( g is identity implies ( P1 . g is identity & P2 . g is identity ) )

assume g is identity ; :: thesis: ( P1 . g is identity & P2 . g is identity )

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_{1}(x)
by A92, A89, Th1

.= f1 by A109 ;

hence P1 . g is identity by A109; :: thesis: P2 . g is identity

P2 . g = P2 . x by CAT_6:def 21, A89

.= H_{2}(x)
by A95, A89, Th1

.= f2 by A109 ;

hence P2 . g is identity by A109; :: thesis: verum

end;assume g is identity ; :: thesis: ( P1 . g is identity & P2 . g is identity )

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

.= f1 by A109 ;

hence P1 . g is identity by A109; :: thesis: P2 . g is identity

P2 . g = P2 . x by CAT_6:def 21, A89

.= H

.= f2 by A109 ;

hence P2 . g is identity by A109; :: thesis: verum

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) )

proof

then
( ( for g1, g2 being morphism of D st g1 |> g2 holds
let g1, g2 be morphism of D; :: thesis: ( g1 |> g2 implies ( P1 . g1 |> P1 . g2 & P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) & P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) ) )

assume g1 |> g2 ; :: thesis: ( P1 . g1 |> P1 . g2 & P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) & P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) )

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_{1}(x1)
by A92, A89, Th1

.= f11 by A111 ;

A113: P1 . g2 = P1 . x2 by CAT_6:def 21, A89

.= H_{1}(x2)
by A92, A89, Th1

.= f12 by A111 ;

A114: P1 . (g1 (*) g2) = P1 . x12 by CAT_6:def 21, A89

.= H_{1}(x12)
by A92, A89, Th1

.= f13 by A111 ;

thus P1 . g1 |> P1 . g2 by A112, A113, A111; :: thesis: ( P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) & P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) )

thus P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) by A112, A113, A114, A111; :: thesis: ( P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) )

A115: P2 . g1 = P2 . x1 by CAT_6:def 21, A89

.= H_{2}(x1)
by A95, A89, Th1

.= f21 by A111 ;

A116: P2 . g2 = P2 . x2 by CAT_6:def 21, A89

.= H_{2}(x2)
by A95, A89, Th1

.= f22 by A111 ;

A117: P2 . (g1 (*) g2) = P2 . x12 by CAT_6:def 21, A89

.= H_{2}(x12)
by A95, A89, Th1

.= f23 by A111 ;

thus P2 . g1 |> P2 . g2 by A115, A116, A111; :: thesis: P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2)

thus P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) by A115, A116, A117, A111; :: thesis: verum

end;assume g1 |> g2 ; :: thesis: ( P1 . g1 |> P1 . g2 & P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) & P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) )

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

.= f11 by A111 ;

A113: P1 . g2 = P1 . x2 by CAT_6:def 21, A89

.= H

.= f12 by A111 ;

A114: P1 . (g1 (*) g2) = P1 . x12 by CAT_6:def 21, A89

.= H

.= f13 by A111 ;

thus P1 . g1 |> P1 . g2 by A112, A113, A111; :: thesis: ( P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) & P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) )

thus P1 . (g1 (*) g2) = (P1 . g1) (*) (P1 . g2) by A112, A113, A114, A111; :: thesis: ( P2 . g1 |> P2 . g2 & P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) )

A115: P2 . g1 = P2 . x1 by CAT_6:def 21, A89

.= H

.= f21 by A111 ;

A116: P2 . g2 = P2 . x2 by CAT_6:def 21, A89

.= H

.= f22 by A111 ;

A117: P2 . (g1 (*) g2) = P2 . x12 by CAT_6:def 21, A89

.= H

.= f23 by A111 ;

thus P2 . g1 |> P2 . g2 by A115, A116, A111; :: thesis: P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2)

thus P2 . (g1 (*) g2) = (P2 . g1) (*) (P2 . g2) by A115, A116, A117, A111; :: thesis: verum

( 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: ( 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 ) ) ) )

for x being object st x in the carrier of D holds

(F1 (*) P1) . x = (F2 (*) P2) . x

proof

hence
F1 (*) P1 = F2 (*) P2
by FUNCT_2:12; :: thesis: for D1 being category
let x be object ; :: thesis: ( x in the carrier of D implies (F1 (*) P1) . x = (F2 (*) P2) . x )

assume A119: x in the carrier of D ; :: thesis: (F1 (*) P1) . x = (F2 (*) P2) . x

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_{1}(x)
by A92, A119

.= f1 by A120 ;

A122: P2 . g = P2 . x by CAT_6:def 21, A89

.= H_{2}(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: verum

end;assume A119: x in the carrier of D ; :: thesis: (F1 (*) P1) . x = (F2 (*) P2) . x

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

.= f1 by A120 ;

A122: P2 . g = P2 . x by CAT_6:def 21, A89

.= H

.= 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: verum

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 ) )

let D1 be category; :: thesis: 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 ) )

let G1 be Functor of D1,C1; :: thesis: 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 ) )

let G2 be Functor of D1,C2; :: thesis: ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 implies 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 ) ) )

assume A123: G1 is covariant ; :: thesis: ( not G2 is covariant or not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A124: G2 is covariant ; :: thesis: ( not F1 (*) G1 = F2 (*) G2 or 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 ) ) )

assume A125: F1 (*) G1 = F2 (*) G2 ; :: thesis: 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 ) )

deffunc H

A126: for x being object st x in the carrier of D1 holds

H

proof

consider H being Function of the carrier of D1, the carrier of D such that
let x be object ; :: thesis: ( x in the carrier of D1 implies H_{3}(x) in the carrier of D )

assume A127: x in the carrier of D1 ; :: thesis: H_{3}(x) in the carrier of D

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_{3}(x) in the carrier of D
by A130, A131; :: thesis: verum

end;assume A127: x in the carrier of D1 ; :: thesis: H

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

A132: for x being object st x in the carrier of D1 holds

H . x = H

reconsider H = H as Functor of D1,D ;

take H ; :: thesis: ( 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 ) )

for d being morphism of D1 st d is identity holds

H . d is identity

proof

then A140:
H is identity-preserving
by CAT_6:def 22;
let d be morphism of D1; :: thesis: ( d is identity implies H . d is identity )

assume A133: d is identity ; :: thesis: H . d is identity

end;assume A133: d is identity ; :: thesis: H . d is identity

per cases
( D1 is empty or not D1 is empty )
;

end;

suppose
D1 is empty
; :: thesis: H . d is identity

then
H . d = the Object of D
by CAT_6:def 21;

hence H . d is identity by A89, CAT_6:22; :: thesis: verum

end;hence H . d is identity by A89, CAT_6:22; :: thesis: verum

suppose A134:
not D1 is empty
; :: thesis: H . d is identity

for g1 being morphism of D st H . d |> g1 holds

(H . d) (*) g1 = g1

for g1 being morphism of D st g1 |> H . d holds

g1 (*) (H . d) = g1

end;(H . d) (*) g1 = g1

proof

then A137:
H . d is left_identity
by CAT_6:def 4;
let g1 be morphism of D; :: thesis: ( H . d |> g1 implies (H . d) (*) g1 = g1 )

assume H . d |> g1 ; :: thesis: (H . d) (*) g1 = g1

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: verum

end;assume H . d |> g1 ; :: thesis: (H . d) (*) g1 = g1

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: verum

for g1 being morphism of D st g1 |> H . d holds

g1 (*) (H . d) = g1

proof

hence
H . d is identity
by A137, CAT_6:def 5, CAT_6:def 14; :: thesis: verum
let g1 be morphism of D; :: thesis: ( g1 |> H . d implies g1 (*) (H . d) = g1 )

assume g1 |> H . d ; :: thesis: g1 (*) (H . d) = g1

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: verum

end;assume g1 |> H . d ; :: thesis: g1 (*) (H . d) = g1

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: verum

for d1, d2 being morphism of D1 st d1 |> d2 holds

( H . d1 |> H . d2 & H . (d1 (*) d2) = (H . d1) (*) (H . d2) )

proof

hence A159:
H is covariant
by A140, CAT_6:def 23, CAT_6:def 25; :: thesis: ( P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
let d1, d2 be morphism of D1; :: thesis: ( d1 |> d2 implies ( H . d1 |> H . d2 & H . (d1 (*) d2) = (H . d1) (*) (H . d2) ) )

assume A141: d1 |> d2 ; :: thesis: ( H . d1 |> H . d2 & H . (d1 (*) d2) = (H . d1) (*) (H . d2) )

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: H . (d1 (*) d2) = (H . d1) (*) (H . d2)

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: verum

end;assume A141: d1 |> d2 ; :: thesis: ( H . d1 |> H . d2 & H . (d1 (*) d2) = (H . d1) (*) (H . d2) )

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: H . (d1 (*) d2) = (H . d1) (*) (H . d2)

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: verum

H = H1 ) )

for x being object st x in the carrier of D1 holds

(P1 (*) H) . x = G1 . x

proof

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

assume A160: x in the carrier of D1 ; :: thesis: (P1 (*) H) . x = G1 . x

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_{1}([(G1 . x),(G2 . x)])
by A92, A89, Th1, A162

.= G1 . x ; :: thesis: verum

end;assume A160: x in the carrier of D1 ; :: thesis: (P1 (*) H) . x = G1 . x

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 ; :: thesis: verum

H = H1 ) )

for x being object st x in the carrier of D1 holds

(P2 (*) H) . x = G2 . x

proof

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

assume A163: x in the carrier of D1 ; :: thesis: (P2 (*) H) . x = G2 . x

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_{2}([(G1 . x),(G2 . x)])
by A165, A95, A89, Th1

.= G2 . x ; :: thesis: verum

end;assume A163: x in the carrier of D1 ; :: thesis: (P2 (*) H) . x = G2 . x

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

.= G2 . x ; :: thesis: verum

H = H1

let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 implies H = H1 )

assume A166: H1 is covariant ; :: thesis: ( not P1 (*) H1 = G1 or not P2 (*) H1 = G2 or H = H1 )

assume A167: P1 (*) H1 = G1 ; :: thesis: ( not P2 (*) H1 = G2 or H = H1 )

assume A168: P2 (*) H1 = G2 ; :: thesis: H = H1

for x being object st x in the carrier of D1 holds

H . x = H1 . x

proof

hence
H = H1
by FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier of D1 implies H . x = H1 . x )

assume A169: x in the carrier of D1 ; :: thesis: H . x = H1 . x

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_{1}([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_{2}([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: verum

end;assume A169: x in the carrier of D1 ; :: thesis: H . x = H1 . x

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 ;

A174: G2 . d = P2 . (H1 . d) by A168, A170, A166, A118, CAT_6:34

.= P2 . x1 by A89, CAT_6:def 21

.= H

.= f2 ;

thus H . x = H1 . d by A173, A174, A172, A171, A169, A132

.= H1 . x by A170, CAT_6:def 21 ; :: thesis: verum

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: ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( 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 )

take P1 ; :: thesis: ex P2 being Functor of D,C2 st

( 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 )

take P2 ; :: thesis: ( 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 )

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: verum