let C, C1, C2 be non empty category; :: thesis:
assume A1: C = Functors (C1,C2) ; :: thesis:
defpred S₁[ object , object ] means ex c being morphism of C ex c1 being morphism of C1 ex d being morphism of (C [x] C1) ex c2 being morphism of C2 ex F12 being Functor of C1,C2 st
( d = [c,c1] & $1 = d & $2 = c2 & c2 = F12 . c1 & F12 = c `2 );
A2: for x being object st x in the carrier of (C [x] C1) holds
ex y being object st
( y in the carrier of C2 & S₁[x,y] )

let x be object ; :: thesis:
assume x in the carrier of (C [x] C1) ; :: thesis:
then reconsider d = x as morphism of (C [x] C1) by CAT_6:def 1;
consider c being morphism of C, c1 being morphism of C1 such that
A3: d = [c,c1] by Th52;
A4: the carrier of (Functors (C1,C2)) = { [[F1,F2],t] where F1, F2 is Functor of C1,C2, t is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } by Def28;
c in Mor C ;
then c in { [[F1,F2],t] where F1, F2 is Functor of C1,C2, t is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } by A4, A1, CAT_6:def 1;
then consider F1, F2 being Functor of C1,C2, t being natural_transformation of F1,F2 such that
A5: ( c = [[F1,F2],t] & F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) ;
reconsider F12 = t as Functor of C1,C2 ;
set c2 = F12 . c1;
reconsider y = F12 . c1 as object ;
take y ; :: thesis:
F12 . c1 in Mor C2 ;
hence y in the carrier of C2 by CAT_6:def 1; :: thesis:
take c ; :: thesis:
take c1 ; :: thesis:
take d ; :: thesis:
take F12 . c1 ; :: thesis:
take F12 ; :: thesis:
thus ( d = [c,c1] & x = d & y = F12 . c1 & F12 . c1 = F12 . c1 & F12 = c `2 ) by A5, A3; :: thesis:

end;

consider E being Function of the carrier of (C [x] C1),C2 such that
A6: for x being object st x in the carrier of (C [x] C1) holds
S₁[x,E . x] from FUNCT_2:sch 1(A2);
reconsider E = E as Functor of (C [x] C1),C2 ;
take E ; :: thesis:
A7: for f being morphism of (C [x] C1) ex c being morphism of C ex c1 being morphism of C1 ex c2 being morphism of C2 ex F12 being Functor of C1,C2 st
( f = [c,c1] & E . f = c2 & c2 = F12 . c1 & F12 = c `2 )

proof

let f be morphism of (C [x] C1); :: thesis:
reconsider x = f as object ;
f in Mor (C [x] C1) ;
then f in the carrier of (C [x] C1) by CAT_6:def 1;
then consider c being morphism of C, c1 being morphism of C1, d being morphism of (C [x] C1), c2 being morphism of C2, F12 being Functor of C1,C2 such that
A8: ( d = [c,c1] & x = d & E . x = c2 & c2 = F12 . c1 & F12 = c `2 ) by A6;
take c ; :: thesis:
take c1 ; :: thesis:
take c2 ; :: thesis:
take F12 ; :: thesis:
thus ( f = [c,c1] & E . f = c2 & c2 = F12 . c1 & F12 = c `2 ) by A8, CAT_6:def 21; :: thesis:

end;

for f being morphism of (C [x] C1) st f is identity holds
E . f is identity

proof

let f be morphism of (C [x] C1); :: thesis:
assume A9: f is identity ; :: thesis:
consider c being morphism of C, c1 being morphism of C1, c2 being morphism of C2, F12 being Functor of C1,C2 such that
A10: ( f = [c,c1] & E . f = c2 & c2 = F12 . c1 & F12 = c `2 ) by A7;
A11: ( c is identity & c1 is identity ) by A9, A10, Th56;
consider F being covariant Functor of C1,C2 such that
A12: c = [[F,F],F] by A1, A11, Th64;
thus E . f is identity by A10, A11, A12, CAT_6:def 22, CAT_6:def 25; :: thesis:

end;

then A13: E is identity-preserving by CAT_6:def 22;
for f1, f2 being morphism of (C [x] C1) st f1 |> f2 holds
( E . f1 |> E . f2 & E . (f1 (*) f2) = (E . f1) (*) (E . f2) )

proof

let f1, f2 be morphism of (C [x] C1); :: thesis:
assume A14: f1 |> f2 ; :: thesis:
consider c1 being morphism of C, c11 being morphism of C1, c12 being morphism of C2, F11 being Functor of C1,C2 such that
A15: ( f1 = [c1,c11] & E . f1 = c12 & c12 = F11 . c11 & F11 = c1 `2 ) by A7;
consider c2 being morphism of C, c21 being morphism of C1, c22 being morphism of C2, F22 being Functor of C1,C2 such that
A16: ( f2 = [c2,c21] & E . f2 = c22 & c22 = F22 . c21 & F22 = c2 `2 ) by A7;
A17: ( c1 |> c2 & c11 |> c21 ) by A14, A15, A16, Th54;
then consider F, F1, F2 being covariant Functor of C1,C2, T1 being natural_transformation of F1,F, T2 being natural_transformation of F,F2 such that
A18: ( c1 = [[F,F2],T2] & c2 = [[F1,F],T1] & c1 (*) c2 = [[F1,F2],(T2 `*` T1)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds
( T2 . g2 |> T1 . g1 & (T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) ) by A1, Th63;
thus E . f1 |> E . f2 by A15, A16, A17, A18; :: thesis:
consider d being morphism of C, d1 being morphism of C1, d2 being morphism of C2, G12 being Functor of C1,C2 such that
A19: ( f1 (*) f2 = [d,d1] & E . (f1 (*) f2) = d2 & d2 = G12 . d1 & G12 = d `2 ) by A7;
A20: [d,d1] = [(c1 (*) c2),(c11 (*) c21)] by A19, A15, A16, A17, Th55;
A21: d = (pr1 (C,C1)) . [d,d1] by Def23
.= c1 (*) c2 by A20, Def23 ;
A22: d1 = (pr2 (C,C1)) . [d,d1] by Def23
.= c11 (*) c21 by A20, Def23 ;
thus E . (f1 (*) f2) = (E . f1) (*) (E . f2) by A15, A16, A18, A17, A21, A19, A22; :: thesis:

end;

hence A23: E is covariant by A13, CAT_6:def 25, CAT_6:def 23; :: thesis:
let D be category; :: thesis:
let F be Functor of (D [x] C1),C2; :: thesis:
assume A24: F is covariant ; :: thesis:

per cases ;

suppose D is empty ; :: thesis:

then reconsider D0 = D as empty category ;
set H = the covariant Functor of D0,C;
reconsider H = the covariant Functor of D0,C as Functor of D,C ;
take H ; :: thesis:
thus ( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) ) ; :: thesis:

end;

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

A26: for d being morphism of D ex F1 being Functor of C1,C2 st
( ( for c1 being morphism of C1 holds F1 . c1 = F . [d,c1] ) & ( d is identity implies F1 is covariant ) )

proof

let d be morphism of D; :: thesis:
defpred S₂[ object , object ] means ex c1 being morphism of C1 st
( $1 = c1 & $2 = F . [d,c1] );
A27: for x being object st x in the carrier of C1 holds
ex y being object st
( y in the carrier of C2 & S₂[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider c1 = x as morphism of C1 by CAT_6:def 1;
set y = F . [d,c1];
take F . [d,c1] ; :: thesis:
F . [d,c1] in Mor C2 ;
hence F . [d,c1] in the carrier of C2 by CAT_6:def 1; :: thesis:
thus S₂[x,F . [d,c1]] ; :: thesis:

end;

consider F1 being Function of the carrier of C1,C2 such that
A28: for x being object st x in the carrier of C1 holds
S₂[x,F1 . x] from FUNCT_2:sch 1(A27);
reconsider F1 = F1 as Functor of C1,C2 ;
take F1 ; :: thesis:
thus A29: for c1 being morphism of C1 holds F1 . c1 = F . [d,c1] :: thesis:

proof

let c1 be morphism of C1; :: thesis:
c1 in Mor C1 ;
then A30: c1 in the carrier of C1 by CAT_6:def 1;
reconsider x = c1 as object ;
consider c2 being morphism of C1 such that
A31: ( x = c2 & F1 . x = F . [d,c2] ) by A28, A30;
thus F1 . c1 = F . [d,c1] by A31, CAT_6:def 21; :: thesis:

end;

thus ( d is identity implies F1 is covariant ) :: thesis:

proof

assume A32: d is identity ; :: thesis:
for c1 being morphism of C1 st c1 is identity holds
F1 . c1 is identity

proof

let c1 be morphism of C1; :: thesis:
assume c1 is identity ; :: thesis:
then A33: [d,c1] is identity by A25, A32, Th56;
F1 . c1 = F . [d,c1] by A29;
hence F1 . c1 is identity by A33, A24, CAT_6:def 25, CAT_6:def 22; :: thesis:

end;

then A34: F1 is identity-preserving by CAT_6:def 22;
for c1, c2 being morphism of C1 st c1 |> c2 holds
( F1 . c1 |> F1 . c2 & F1 . (c1 (*) c2) = (F1 . c1) (*) (F1 . c2) )

proof

let c1, c2 be morphism of C1; :: thesis:
assume A35: c1 |> c2 ; :: thesis:
A36: d |> d by A25, A32, CAT_6:24;
A37: [d,c1] |> [d,c2] by A35, A36, Th54;
A38: F is multiplicative by A24, CAT_6:def 25;
A39: ( F1 . c1 = F . [d,c1] & F1 . c2 = F . [d,c2] ) by A29;
hence F1 . c1 |> F1 . c2 by A38, A37, CAT_6:def 23; :: thesis:
thus F1 . (c1 (*) c2) = F . [d,(c1 (*) c2)] by A29
.= F . [(d (*) d),(c1 (*) c2)] by A36, A32, Th4
.= F . ([d,c1] (*) [d,c2]) by A35, A36, Th55
.= (F1 . c1) (*) (F1 . c2) by A38, A39, A37, CAT_6:def 23 ; :: thesis:

end;

hence F1 is covariant by A34, CAT_6:def 25, CAT_6:def 23; :: thesis:

end;

defpred S₂[ object , object ] means ex d, d1, d2 being morphism of D ex F1, F2 being Functor of C1,C2 ex T being natural_transformation of F1,F2 st
( $1 = d & d2 |> d & d |> d1 & d1 is identity & d2 is identity & $2 = [[F1,F2],T] & F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 & ( for c1 being morphism of C1 holds
( F1 . c1 = F . [d1,c1] & F2 . c1 = F . [d2,c1] & T . c1 = F . [d,c1] ) ) );
A40: for x being object st x in the carrier of D holds
ex y being object st
( y in the carrier of C & S₂[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of D ; :: thesis:
then reconsider d = x as morphism of D by CAT_6:def 1;
consider d2, d1 being morphism of D such that
A41: ( d2 is identity & d1 is identity & d2 |> d & d |> d1 ) by A25, Th5;
consider F1 being Functor of C1,C2 such that
A42: ( ( for c1 being morphism of C1 holds F1 . c1 = F . [d1,c1] ) & ( d1 is identity implies F1 is covariant ) ) by A26;
consider F2 being Functor of C1,C2 such that
A43: ( ( for c1 being morphism of C1 holds F2 . c1 = F . [d2,c1] ) & ( d2 is identity implies F2 is covariant ) ) by A26;
consider T being Functor of C1,C2 such that
A44: ( ( for c1 being morphism of C1 holds T . c1 = F . [d,c1] ) & ( d is identity implies T is covariant ) ) by A26;
for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )

proof

let f, f1, f2 be morphism of C1; :: thesis:
assume A45: ( f1 is identity & f2 is identity ) ; :: thesis:
assume A46: ( f1 |> f & f |> f2 ) ; :: thesis:
A47: ( T . f1 = F . [d,f1] & T . f2 = F . [d,f2] ) by A44;
A48: F1 . f = F . [d1,f] by A42;
A49: F2 . f = F . [d2,f] by A43;
A50: F is multiplicative by A24, CAT_6:def 25;
A51: [d,f1] |> [d1,f] by A46, A41, Th54;
thus T . f1 |> F1 . f by A47, A48, A51, A50, CAT_6:def 23; :: thesis:
A52: [d2,f] |> [d,f2] by A46, A41, Th54;
hence F2 . f |> T . f2 by A49, A47, A50, CAT_6:def 23; :: thesis:
thus T . f = F . [d,f] by A44
.= F . [d,(f1 (*) f)] by A46, A45, Th4
.= F . [(d (*) d1),(f1 (*) f)] by A41, Th4
.= F . ([d,f1] (*) [d1,f]) by A46, A41, Th55
.= (F . [d,f1]) (*) (F . [d1,f]) by A51, A50, CAT_6:def 23
.= (T . f1) (*) (F1 . f) by A48, A44 ; :: thesis:
thus T . f = F . [d,f] by A44
.= F . [d,(f (*) f2)] by A46, A45, Th4
.= F . [(d2 (*) d),(f (*) f2)] by A41, Th4
.= F . ([d2,f] (*) [d,f2]) by A46, A41, Th55
.= (F . [d2,f]) (*) (F . [d,f2]) by A52, A50, CAT_6:def 23
.= (F2 . f) (*) (T . f2) by A49, A44 ; :: thesis:

end;

then A53: T is_natural_transformation_of F1,F2 by Th58, A42, A43, A41;
then A54: F1 is_naturally_transformable_to F2 ;
then reconsider T = T as natural_transformation of F1,F2 by A53, Def26;
set y = [[F1,F2],T];
take [[F1,F2],T] ; :: thesis:
[[F1,F2],T] in { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } by A54, A42, A43, A41;
hence [[F1,F2],T] in the carrier of C by A1, Def28; :: thesis:
thus S₂[x,[[F1,F2],T]] by A41, A42, A43, A44, A54; :: thesis:

end;

consider H being Function of the carrier of D,C such that
A55: for x being object st x in the carrier of D holds
S₂[x,H . x] from FUNCT_2:sch 1(A40);
reconsider H = H as Functor of D,C ;
take H ; :: thesis:
A56: for f being morphism of D st f is identity holds
H . f is identity

proof

let f be morphism of D; :: thesis:
assume A57: f is identity ; :: thesis:
reconsider x = f as object ;
not Mor D is empty by A25;
then f in Mor D ;
then x in the carrier of D by CAT_6:def 1;
then consider d, d1, d2 being morphism of D, F1, F2 being Functor of C1,C2, T being natural_transformation of F1,F2 such that
A58: ( x = d & d2 |> d & d |> d1 & d1 is identity & d2 is identity & H . x = [[F1,F2],T] & F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 & ( for c1 being morphism of C1 holds
( F1 . c1 = F . [d1,c1] & F2 . c1 = F . [d2,c1] & T . c1 = F . [d,c1] ) ) ) by A55;
A59: d2 = d2 (*) d by A58, A57, Th4
.= d by A58, Th4 ;
A60: d1 = d (*) d1 by A58, A57, Th4
.= d by A58, Th4 ;
for x being object st x in the carrier of C1 holds
F1 . x = F2 . x

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider c1 = x as morphism of C1 by CAT_6:def 1;
thus F1 . x = F1 . c1 by CAT_6:def 21
.= F . [d1,c1] by A58
.= F2 . c1 by A58, A59, A60
.= F2 . x by CAT_6:def 21 ; :: thesis:

end;

then A61: F1 = F2 by FUNCT_2:12;
A62: for x being object st x in the carrier of C1 holds
F2 . x = T . x

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider c1 = x as morphism of C1 by CAT_6:def 1;
thus F2 . x = F2 . c1 by CAT_6:def 21
.= F . [d2,c1] by A58
.= T . c1 by A58, A59
.= T . x by CAT_6:def 21 ; :: thesis:

end;

H . f = H . x by A25, CAT_6:def 21
.= [[F1,F1],F1] by A58, A62, A61, FUNCT_2:12 ;
hence H . f is identity by A1, A58, Th64; :: thesis:

end;

then A63: H is identity-preserving by CAT_6:def 22;
for f1, f2 being morphism of D st f1 |> f2 holds
( H . f1 |> H . f2 & H . (f1 (*) f2) = (H . f1) (*) (H . f2) )

proof

let f1, f2 be morphism of D; :: thesis:
assume A64: f1 |> f2 ; :: thesis:
reconsider x1 = f1, x2 = f2 as object ;
A65: not Mor D is empty by A25;
then ( f1 in Mor D & f2 in Mor D ) ;
then A66: ( x1 in the carrier of D & x2 in the carrier of D ) by CAT_6:def 1;
consider d1, d11, d12 being morphism of D, F11, F12 being Functor of C1,C2, T1 being natural_transformation of F11,F12 such that
A67: ( x2 = d1 & d12 |> d1 & d1 |> d11 & d11 is identity & d12 is identity & H . x2 = [[F11,F12],T1] & F11 is covariant & F12 is covariant & F11 is_naturally_transformable_to F12 & ( for c1 being morphism of C1 holds
( F11 . c1 = F . [d11,c1] & F12 . c1 = F . [d12,c1] & T1 . c1 = F . [d1,c1] ) ) ) by A66, A55;
consider d2, d21, d22 being morphism of D, F21, F22 being Functor of C1,C2, T2 being natural_transformation of F21,F22 such that
A68: ( x1 = d2 & d22 |> d2 & d2 |> d21 & d21 is identity & d22 is identity & H . x1 = [[F21,F22],T2] & F21 is covariant & F22 is covariant & F21 is_naturally_transformable_to F22 & ( for c1 being morphism of C1 holds
( F21 . c1 = F . [d21,c1] & F22 . c1 = F . [d22,c1] & T2 . c1 = F . [d2,c1] ) ) ) by A66, A55;
reconsider x12 = f1 (*) f2 as object ;
f1 (*) f2 in Mor D by A65;
then A69: x12 in the carrier of D by CAT_6:def 1;
consider d3, d31, d32 being morphism of D, F31, F32 being Functor of C1,C2, T3 being natural_transformation of F31,F32 such that
A70: ( x12 = d3 & d32 |> d3 & d3 |> d31 & d31 is identity & d32 is identity & H . x12 = [[F31,F32],T3] & F31 is covariant & F32 is covariant & F31 is_naturally_transformable_to F32 & ( for c1 being morphism of C1 holds
( F31 . c1 = F . [d31,c1] & F32 . c1 = F . [d32,c1] & T3 . c1 = F . [d3,c1] ) ) ) by A69, A55;
A71: dom d2 = cod d1 by A25, CAT_7:5, A64, A67, A68;
A72: d12 = cod d1 by A67, CAT_6:27
.= d21 by A71, A68, CAT_6:26 ;
A73: for x being object st x in the carrier of C1 holds
F12 . x = F21 . x

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider c1 = x as morphism of C1 by CAT_6:def 1;
thus F12 . x = F12 . c1 by CAT_6:def 21
.= F . [d12,c1] by A67
.= F21 . c1 by A72, A68
.= F21 . x by CAT_6:def 21 ; :: thesis:

end;

then A74: F12 = F21 by FUNCT_2:12;
reconsider T2 = T2 as natural_transformation of F12,F22 by A73, FUNCT_2:12;
A75: d31 = dom (f1 (*) f2) by A70, CAT_6:26
.= dom d1 by A67, A64, CAT_7:4
.= d11 by A67, CAT_6:26 ;
for x being object st x in the carrier of C1 holds
F31 . x = F11 . x

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider c1 = x as morphism of C1 by CAT_6:def 1;
thus F31 . x = F31 . c1 by CAT_6:def 21
.= F . [d31,c1] by A70
.= F11 . c1 by A75, A67
.= F11 . x by CAT_6:def 21 ; :: thesis:

end;

then A76: F31 = F11 by FUNCT_2:12;
A77: d32 = cod (f1 (*) f2) by A70, CAT_6:27
.= cod d2 by A68, A64, CAT_7:4
.= d22 by A68, CAT_6:27 ;
for x being object st x in the carrier of C1 holds
F32 . x = F22 . x

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider c1 = x as morphism of C1 by CAT_6:def 1;
thus F32 . x = F32 . c1 by CAT_6:def 21
.= F . [d32,c1] by A70
.= F22 . c1 by A77, A68
.= F22 . x by CAT_6:def 21 ; :: thesis:

end;

then A78: F32 = F22 by FUNCT_2:12;
A79: for x being object st x in the carrier of C1 holds
T3 . x = (T2 `*` T1) . x

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider c = x as morphism of C1 by CAT_6:def 1;
consider c2, c1 being morphism of C1 such that
A80: ( c2 is identity & c1 is identity & c2 |> c & c |> c1 ) by Th5;
A81: F is multiplicative by A24, CAT_6:def 25;
A82: [d2,c2] |> [d12,c] by A80, Th54, A68, A72;
A83: [d2,c2] (*) [d12,c] = [(d2 (*) d12),(c2 (*) c)] by A72, A68, A80, Th55
.= [d2,(c2 (*) c)] by A72, A68, Th4
.= [d2,c] by A80, Th4 ;
A84: [d2,c] |> [d1,c1] by A80, A64, A67, A68, Th54;
A85: [d2,c] (*) [d1,c1] = [(d2 (*) d1),(c (*) c1)] by A64, A67, A68, A80, Th55
.= [d3,c] by A70, A80, A67, A68, Th4 ;
thus T3 . x = T3 . c by CAT_6:def 21
.= F . ([d2,c] (*) [d1,c1]) by A85, A70
.= (F . ([d2,c2] (*) [d12,c])) (*) (F . [d1,c1]) by A83, A81, A84, CAT_6:def 23
.= ((F . [d2,c2]) (*) (F . [d12,c])) (*) (F . [d1,c1]) by A82, A81, CAT_6:def 23
.= ((F . [d2,c2]) (*) (F . [d12,c])) (*) (T1 . c1) by A67
.= ((F . [d2,c2]) (*) (F12 . c)) (*) (T1 . c1) by A67
.= ((T2 . c2) (*) (F12 . c)) (*) (T1 . c1) by A68
.= (T2 `*` T1) . c by A74, A67, A68, A80, Def27
.= (T2 `*` T1) . x by CAT_6:def 21 ; :: thesis:

end;

A86: H . f1 = H . x1 by A25, CAT_6:def 21
.= [[F12,F22],T2] by A73, A68, FUNCT_2:12 ;
A87: H . f2 = [[F11,F12],T1] by A67, A25, CAT_6:def 21;
A88: H . (f1 (*) f2) = [[F31,F32],T3] by A70, A25, CAT_6:def 21
.= [[F11,F22],(T2 `*` T1)] by A76, A78, A79, FUNCT_2:12 ;
A89: the carrier of C = { [[F1,F2],t] where F1, F2 is Functor of C1,C2, t is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } by A1, Def28;
H . x1 in the carrier of C by A68, A89;
then A90: H . f1 is Element of the carrier of C by A25, CAT_6:def 21;
H . x2 in the carrier of C by A67, A89;
then A91: H . f2 is Element of the carrier of C by A25, CAT_6:def 21;
H . x12 in the carrier of C by A70, A89;
then A92: H . (f1 (*) f2) is Element of the carrier of C by A25, CAT_6:def 21;
[(KuratowskiPair ((H . f1),(H . f2))),(H . (f1 (*) f2))] in { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of C : ex F1, F2, F3 being Functor of C1,C2 ex t1 being natural_transformation of F1,F2 ex t2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],t1] & x2 = [[F2,F3],t2] & x3 = [[F1,F3],(t2 `*` t1)] ) } by A86, A87, A88, A90, A91, A92;
then A93: [(KuratowskiPair ((H . f1),(H . f2))),(H . (f1 (*) f2))] in the composition of C by A1, Def28;
then A94: KuratowskiPair ((H . f1),(H . f2)) in dom the composition of C by XTUPLE_0:def 12;
hence H . f1 |> H . f2 by CAT_6:def 2; :: thesis:
thus H . (f1 (*) f2) = the composition of C . (KuratowskiPair ((H . f1),(H . f2))) by A94, A93, FUNCT_1:def 2
.= the composition of C . ((H . f1),(H . f2)) by BINOP_1:def 1
.= (H . f1) (*) (H . f2) by A94, CAT_6:def 3, CAT_6:def 2 ; :: thesis:

end;

hence A95: H is covariant by A63, CAT_6:def 25, CAT_6:def 23; :: thesis:
A96: for d being morphism of D
for c1 being morphism of C1 holds F . [d,c1] = E . [(H . d),c1]

proof

let d be morphism of D; :: thesis:
let c1 be morphism of C1; :: thesis:
reconsider x = [(H . d),c1] as object ;
[(H . d),c1] in Mor (C [x] C1) ;
then x in the carrier of (C [x] C1) by CAT_6:def 1;
then consider c being morphism of C, c11 being morphism of C1, d1 being morphism of (C [x] C1), c22 being morphism of C2, F12 being Functor of C1,C2 such that
A97: ( d1 = [c,c11] & x = d1 & E . x = c22 & c22 = F12 . c11 & F12 = c `2 ) by A6;
A98: ( H . d = c & c1 = c11 ) by A97, Th53;
reconsider x1 = d as object ;
not Mor D is empty by A25;
then d in Mor D ;
then x1 in the carrier of D by CAT_6:def 1;
then consider d1, d11, d12 being morphism of D, F1, F2 being Functor of C1,C2, T being natural_transformation of F1,F2 such that
A99: ( x1 = d1 & d12 |> d1 & d1 |> d11 & d11 is identity & d12 is identity & H . x1 = [[F1,F2],T] & F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 & ( for c1 being morphism of C1 holds
( F1 . c1 = F . [d11,c1] & F2 . c1 = F . [d12,c1] & T . c1 = F . [d1,c1] ) ) ) by A55;
A100: H . d = [[F1,F2],T] by A99, A25, CAT_6:def 21;
thus F . [d,c1] = E . x by A97, A98, A100, A99
.= E . [(H . d),c1] by CAT_6:def 21 ; :: thesis:

end;

A101: for c1 being morphism of C1 holds (id C1) . c1 = c1

proof

let c1 be morphism of C1; :: thesis:
reconsider x1 = c1 as object ;
x1 in Mor C1 ;
then A102: x1 in the carrier of C1 by CAT_6:def 1;
thus (id C1) . c1 = (id C1) . x1 by CAT_6:def 21
.= (id the carrier of C1) . x1 by STRUCT_0:def 4
.= c1 by A102, FUNCT_1:18 ; :: thesis:

end;

A103: for x being object st x in the carrier of (D [x] C1) holds
F . x = (E (*) (H [x] (id C1))) . x

proof

let x be object ; :: thesis:
assume x in the carrier of (D [x] C1) ; :: thesis:
then reconsider f = x as morphism of (D [x] C1) by CAT_6:def 1;
A104: H [x] (id C1) is covariant by A95, Def22;
consider d being morphism of D, c1 being morphism of C1 such that
A105: f = [d,c1] by Th52;
thus F . x = F . [d,c1] by A105, A25, CAT_6:def 21
.= E . [(H . d),c1] by A96
.= E . [(H . d),((id C1) . c1)] by A101
.= E . ((H [x] (id C1)) . f) by A105, A25, A95, Th57
.= (E (*) (H [x] (id C1))) . f by A23, A104, A25, CAT_6:34
.= (E (*) (H [x] (id C1))) . x by A25, CAT_6:def 21 ; :: thesis:

end;

hence F = E (*) (H [x] (id C1)) by FUNCT_2:12; :: thesis:
let H1 be Functor of D,C; :: thesis:
assume A106: H1 is covariant ; :: thesis:
assume A107: F = E (*) (H1 [x] (id C1)) ; :: thesis:
A108: for d being morphism of D st d is identity holds
H . d = H1 . d

proof

let d be morphism of D; :: thesis:
assume A109: d is identity ; :: thesis:
then consider F1 being covariant Functor of C1,C2 such that
A110: H . d = [[F1,F1],F1] by A1, Th64, A56;
H1 is identity-preserving by A106, CAT_6:def 25;
then consider F2 being covariant Functor of C1,C2 such that
A111: H1 . d = [[F2,F2],F2] by A1, Th64, A109, CAT_6:def 22;
F1 = F2

proof

assume F1 <> F2 ; :: thesis:
then consider x being object such that
A112: ( x in the carrier of C1 & F1 . x <> F2 . x ) by FUNCT_2:12;
reconsider c1 = x as morphism of C1 by A112, CAT_6:def 1;
A113: H [x] (id C1) is covariant by A95, Def22;
A114: (E (*) (H [x] (id C1))) . [d,c1] = E . ((H [x] (id C1)) . [d,c1]) by A25, A23, A113, CAT_6:34
.= E . [(H . d),((id C1) . c1)] by A25, A95, Th57
.= E . [(H . d),c1] by A101 ;
consider c01 being morphism of C, c11 being morphism of C1, c12 being morphism of C2, F12 being Functor of C1,C2 such that
A115: ( [(H . d),c1] = [c01,c11] & E . [(H . d),c1] = c12 & c12 = F12 . c11 & F12 = c01 `2 ) by A7;
A116: ( H . d = c01 & c1 = c11 ) by A115, Th53;
A117: H1 [x] (id C1) is covariant by A106, Def22;
A118: (E (*) (H1 [x] (id C1))) . [d,c1] = E . ((H1 [x] (id C1)) . [d,c1]) by A25, A23, A117, CAT_6:34
.= E . [(H1 . d),((id C1) . c1)] by A106, A25, Th57
.= E . [(H1 . d),c1] by A101 ;
consider c02 being morphism of C, c21 being morphism of C1, c22 being morphism of C2, F22 being Functor of C1,C2 such that
A119: ( [(H1 . d),c1] = [c02,c21] & E . [(H1 . d),c1] = c22 & c22 = F22 . c21 & F22 = c02 `2 ) by A7;
A120: ( H1 . d = c02 & c1 = c21 ) by A119, Th53;
F1 . x = F1 . c1 by CAT_6:def 21
.= F2 . c1 by A110, A111, A120, A115, A116, A119, A114, A118, A103, A107, FUNCT_2:12
.= F2 . x by CAT_6:def 21 ;
hence contradiction by A112; :: thesis:

end;

hence H . d = H1 . d by A110, A111; :: thesis:

end;

for x being object st x in the carrier of D holds
H . x = H1 . x

proof

let x be object ; :: thesis:
assume x in the carrier of D ; :: thesis:
then reconsider d = x as morphism of D by CAT_6:def 1;
consider d1, d2 being morphism of D such that
A121: ( d1 is identity & d2 is identity & d1 |> d & d |> d2 ) by A25, Th5;
A122: ( dom d = d2 & cod d = d1 ) by A121, CAT_6:26, CAT_6:27;
A123: ( H . d1 = H1 . d1 & H . d2 = H1 . d2 ) by A121, A108;
A124: dom (H . d) = H . (dom d) by A25, A95, CAT_6:32
.= H1 . d2 by A25, A122, A123, CAT_6:def 21
.= H1 . (dom d) by A25, A122, CAT_6:def 21
.= dom (H1 . d) by A25, A106, CAT_6:32 ;
A125: cod (H . d) = H . (cod d) by A25, A95, CAT_6:32
.= H1 . d1 by A25, A122, A123, CAT_6:def 21
.= H1 . (cod d) by A25, A122, CAT_6:def 21
.= cod (H1 . d) by A25, A106, CAT_6:32 ;
consider F1, F2 being covariant Functor of C1,C2, T being natural_transformation of F1,F2 such that
A126: ( H . d = [[F1,F2],T] & dom (H . d) = [[F1,F1],F1] & cod (H . d) = [[F2,F2],F2] ) by A1, Th65;
consider F11, F12 being covariant Functor of C1,C2, T1 being natural_transformation of F11,F12 such that
A127: ( H1 . d = [[F11,F12],T1] & dom (H1 . d) = [[F11,F11],F11] & cod (H1 . d) = [[F12,F12],F12] ) by A1, Th65;
A128: F1 = F11 by A126, A127, A124, XTUPLE_0:1;
A129: F2 = F12 by A126, A127, A125, XTUPLE_0:1;
A130: T = T1

proof

assume T <> T1 ; :: thesis:
then consider x being object such that
A131: ( x in the carrier of C1 & T . x <> T1 . x ) by FUNCT_2:12;
reconsider c1 = x as morphism of C1 by A131, CAT_6:def 1;
A132: (E (*) (H [x] (id C1))) . [d,c1] = (E (*) (H1 [x] (id C1))) . [d,c1] by A103, FUNCT_2:12, A107;
A133: H [x] (id C1) is covariant by A95, Def22;
A134: (E (*) (H [x] (id C1))) . [d,c1] = E . ((H [x] (id C1)) . [d,c1]) by A25, A23, A133, CAT_6:34
.= E . [(H . d),((id C1) . c1)] by A25, A95, Th57
.= E . [(H . d),c1] by A101 ;
consider c01 being morphism of C, c11 being morphism of C1, c12 being morphism of C2, F12 being Functor of C1,C2 such that
A135: ( [(H . d),c1] = [c01,c11] & E . [(H . d),c1] = c12 & c12 = F12 . c11 & F12 = c01 `2 ) by A7;
A136: ( H . d = c01 & c1 = c11 ) by A135, Th53;
A137: H1 [x] (id C1) is covariant by A106, Def22;
A138: (E (*) (H1 [x] (id C1))) . [d,c1] = E . ((H1 [x] (id C1)) . [d,c1]) by A25, A23, A137, CAT_6:34
.= E . [(H1 . d),((id C1) . c1)] by A106, A25, Th57
.= E . [(H1 . d),c1] by A101 ;
consider c02 being morphism of C, c21 being morphism of C1, c22 being morphism of C2, F22 being Functor of C1,C2 such that
A139: ( [(H1 . d),c1] = [c02,c21] & E . [(H1 . d),c1] = c22 & c22 = F22 . c21 & F22 = c02 `2 ) by A7;
A140: ( H1 . d = c02 & c1 = c21 ) by A139, Th53;
T . x = T . c1 by CAT_6:def 21;
hence contradiction by A131, A136, A135, A126, A140, A139, A127, CAT_6:def 21, A132, A134, A138; :: thesis:

end;

thus H . x = H1 . d by A130, A25, A126, A127, A128, A129, CAT_6:def 21
.= H1 . x by A25, CAT_6:def 21 ; :: thesis:

end;

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

end;