let A, B, C be Category; :: thesis:
let F1, F2 be Functor of [:A,B:],C; :: thesis:
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis:
then A2: F1 is_transformable_to F2 ;
let t be natural_transformation of F1,F2; :: thesis:
reconsider s = t as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;

let a be Object of A; :: thesis:
let S1, S2 be Functor of B,C; :: thesis:
assume that
A4: S1 = (export F1) . a and
A5: S2 = (export F2) . a ; :: thesis:
let b be Object of B; :: thesis:
A6: S2 . b = (F2 ?- a) . b by A5, Th18
.= F2 . [a,b] by Th8 ;
A7: ((curry s) . a) . b = s . (a,b) by FUNCT_5:69
.= t . [a,b] by A2, NATTRA_1:def 5 ;
S1 . b = (F1 ?- a) . b by A4, Th18
.= F1 . [a,b] by Th8 ;
hence ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A2, A6, A7, Lm1; :: thesis:

end;

A8: for a being Object of A
for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds
S1 is_transformable_to S2 by A3;

A9: now :: thesis:

let a be Object of A; :: thesis:
let S1, S2 be Functor of B,C; :: thesis:
let T be transformation of S1,S2; :: thesis:
assume that
A10: S1 = (export F1) . a and
A11: S2 = (export F2) . a and
A12: T = (curry s) . a ; :: thesis:
let b1, b2 be Object of B; :: thesis:
assume A13: Hom (b1,b2) <> {} ; :: thesis:
A14: Hom ((S1 . b1),(S1 . b2)) <> {} by A13, CAT_1:84;
A15: T . b2 = T . b2 by A8, A10, A11, NATTRA_1:def 5
.= s . (a,b2) by A12, FUNCT_5:69
.= t . [a,b2] by A2, NATTRA_1:def 5 ;
A16: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2;
let f be Morphism of b1,b2; :: thesis:
A17: Hom (a,a) <> {} ;
then reconsider g = [(id a),f] as Morphism of [a,b1],[a,b2] by A13, CAT_2:33;
A18: Hom ([a,b1],[a,b2]) <> {} by A13, A17, Th9;
then A19: Hom ((F1 . [a,b1]),(F1 . [a,b2])) <> {} by CAT_1:84;
A20: S1 is_transformable_to S2 by A8, A10, A11;
then A21: Hom ((S1 . b1),(S2 . b1)) <> {} ;
A22: T . b1 = T . b1 by A8, A10, A11, NATTRA_1:def 5
.= s . (a,b1) by A12, FUNCT_5:69
.= t . [a,b1] by A2, NATTRA_1:def 5 ;
A23: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2;
A24: Hom ((S1 . b2),(S2 . b2)) <> {} by A20;
A25: Hom ((S2 . b1),(S2 . b2)) <> {} by A13, CAT_1:84;
A26: S2 /. f = (F2 ?- a) /. f by A11, Th18
.= (F2 ?- a) /. f by A13, CAT_3:def 10
.= F2 . ((id a),f) by CAT_2:36
.= F2 /. g by A18, CAT_3:def 10 ;
A27: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A18, CAT_1:84;
A28: S1 /. f = (F1 ?- a) /. f by A10, Th18
.= (F1 ?- a) /. f by A13, CAT_3:def 10
.= F1 . ((id a),f) by CAT_2:36
.= F1 /. g by A18, CAT_3:def 10 ;
thus (T . b2) * (S1 /. f) = (T . b2) (*) (S1 /. f) by A14, A24, CAT_1:def 13
.= (t . [a,b2]) * (F1 /. g) by A19, A16, A15, A28, CAT_1:def 13
.= (F2 /. g) * (t . [a,b1]) by A1, A18, NATTRA_1:def 8
.= (S2 /. f) (*) (T . b1) by A27, A23, A22, A26, CAT_1:def 13
.= (S2 /. f) * (T . b1) by A25, A21, CAT_1:def 13 ; :: thesis:

end;

defpred S₁[ object , object ] means for f being Object of A
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s & $1 = f holds
$2 = [[((export F1) . f),((export F2) . f)],((curry s) . f)];

A29: now :: thesis:

let a be Object of A; :: thesis:
let S1, S2 be Functor of B,C; :: thesis:
assume A30: ( S1 = (export F1) . a & S2 = (export F2) . a ) ; :: thesis:
thus (curry s) . a is transformation of S1,S2 :: thesis:

proof

thus S1 is_transformable_to S2 by A8, A30; :: according to NATTRA_1:def 3 :: thesis:
let b be Object of B; :: thesis:
((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A3, A30;
hence ((curry s) . a) . b is Morphism of S1 . b,S2 . b by CAT_1:def 5; :: thesis:

end;

A31: now :: thesis:

let m be object ; :: thesis:
assume m in the carrier of A ; :: thesis:
then reconsider a = m as Object of A ;
reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th19;
reconsider o = [[((export F1) . a),((export F2) . a)],((curry s) . a)] as object ;
take o = o; :: thesis:
reconsider T = (curry s) . a as transformation of S1,S2 by A29;
A32: S1 is_naturally_transformable_to S2

proof

thus S1 is_transformable_to S2 by A8; :: according to NATTRA_1:def 7 :: thesis:
take T ; :: thesis:
thus for b₁, b₂ being Element of the carrier of B holds
( Hom (b₁,b₂) = {} or for b₃ being Morphism of b₁,b₂ holds (T . b₂) * (S1 /. b₃) = (S2 /. b₃) * (T . b₁) ) by A9; :: thesis:

end;

for a, b being Object of B st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (T . b) * (S1 /. f) = (S2 /. f) * (T . a) by A9;
then T is natural_transformation of S1,S2 by A32, NATTRA_1:def 8;
then o in NatTrans (B,C) by A32, NATTRA_1:32;
hence o in the carrier' of (Functors (B,C)) by NATTRA_1:def 17; :: thesis:
thus S₁[m,o] ; :: thesis:

end;

consider G being Function of the carrier of A, the carrier' of (Functors (B,C)) such that
A33: for m being object st m in the carrier of A holds
S₁[m,G . m] from FUNCT_2:sch 1(A31);

A34: now :: thesis:

let a be Object of A; :: thesis:
reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th19;
reconsider T = (curry s) . a as transformation of S1,S2 by A29;
A35: G . a = [[S1,S2],T] by A33;
A36: S1 is_naturally_transformable_to S2

proof

end;

for a, b being Object of B st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (T . b) * (S1 /. f) = (S2 /. f) * (T . a) by A9;
then T is natural_transformation of S1,S2 by A36, NATTRA_1:def 8;
then ( dom (G . a) = S1 & cod (G . a) = S2 ) by A35, NATTRA_1:33;
hence G . a in Hom (((export F1) . a),((export F2) . a)) ; :: thesis:

end;

then A37: for a being Object of A holds Hom (((export F1) . a),((export F2) . a)) <> {} ;
G is transformation of export F1, export F2

proof

thus export F1 is_transformable_to export F2 by A37; :: according to NATTRA_1:def 3 :: thesis:
let a be Object of A; :: thesis:
G . a in Hom (((export F1) . a),((export F2) . a)) by A34;
hence G . a is Morphism of (export F1) . a,(export F2) . a by CAT_1:def 5; :: thesis:

end;

then reconsider G = G as transformation of export F1, export F2 ;
A38: export F1 is_transformable_to export F2 by A37;

A39: now :: thesis:

let a, b be Object of A; :: thesis:
assume A40: Hom (a,b) <> {} ; :: thesis:
A41: Hom (((export F2) . a),((export F2) . b)) <> {} by A40, CAT_1:84;
reconsider S1 = (export F1) . a, S2 = (export F2) . a, S3 = (export F1) . b, S4 = (export F2) . b as Functor of B,C by Th19;
let f be Morphism of a,b; :: thesis:
A42: F2 ?- a = (export F2) . a by Th18;
A43: F1 ?- a = (export F1) . a by Th18;
then reconsider T12 = (curry s) . a as natural_transformation of S1,S2 by A1, A42, Th11;
A44: F2 ?- b = (export F2) . b by Th18;
then A45: F2 ?- (cod f) = (export F2) . b by A40, CAT_1:5;
then reconsider T24 = F2 ?- f as natural_transformation of S2,S4 by A40, A42, CAT_1:5;
A46: G . a = G . a by A38, NATTRA_1:def 5
.= [[S1,S2],T12] by A33 ;
A47: F1 ?- b = (export F1) . b by Th18;
then reconsider T34 = (curry s) . b as natural_transformation of S3,S4 by A1, A44, Th11;
A48: S3 is_naturally_transformable_to S4 by A1, A47, A44, Th11;
then A49: S3 is_transformable_to S4 ;
A50: F1 ?- (cod f) = (export F1) . b by A40, A47, CAT_1:5;
then reconsider T13 = F1 ?- f as natural_transformation of S1,S3 by A40, A43, CAT_1:5;
A51: G . b = G . b by A38, NATTRA_1:def 5
.= [[S3,S4],T34] by A33 ;
A52: S1 is_naturally_transformable_to S2 by A1, A42, A43, Th11;
then A53: S1 is_transformable_to S2 ;
reconsider g = f as Morphism of A ;
A54: Hom (((export F1) . a),((export F2) . a)) <> {} by A34;
F2 ?- (dom f) = (export F2) . a by A40, A42, CAT_1:5;
then A55: (export F2) . g = [[S2,S4],T24] by A45, Def4;
A56: Hom (((export F1) . a),((export F1) . b)) <> {} by A40, CAT_1:84;
A57: S2 is_naturally_transformable_to S4 by A40, A42, A44, Th13;
then A58: S2 is_transformable_to S4 ;
A59: S1 is_naturally_transformable_to S3 by A40, A47, A43, Th13;
then A60: S1 is_transformable_to S3 ;

now :: thesis:

reconsider FF1 = F1, FF2 = F2 as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
let c be Object of B; :: thesis:
A61: Hom ((F1 . [a,c]),(F2 . [a,c])) <> {} by A2;
A62: Hom ((F1 . [b,c]),(F2 . [b,c])) <> {} by A2;
A63: ( Hom ((S3 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S3 . c)) <> {} ) by A60, A49;
A64: ( Hom ((S2 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S2 . c)) <> {} ) by A53, A58;
A65: t . [b,c] = s . (b,c) by A2, NATTRA_1:def 5
.= ((curry s) . b) . c by FUNCT_5:69
.= T34 . c by A49, NATTRA_1:def 5 ;
A66: t . [a,c] = s . (a,c) by A2, NATTRA_1:def 5
.= ((curry s) . a) . c by FUNCT_5:69
.= T12 . c by A53, NATTRA_1:def 5 ;
A67: Hom (c,c) <> {} ;
then reconsider fi = [f,(id c)] as Morphism of [a,c],[b,c] by A40, CAT_2:33;
A68: Hom ([a,c],[b,c]) <> {} by A40, A67, Th9;
then A69: Hom ((F2 . [a,c]),(F2 . [b,c])) <> {} by CAT_1:84;
A70: id c = (IdMap B) . c by ISOCAT_1:def 12;
A71: F1 /. fi = FF1 . (f,(id c)) by A68, CAT_3:def 10
.= (curry (F1,f)) . (id c) by FUNCT_5:69
.= (F1 ?- f) . c by A70, FUNCT_2:15
.= T13 . c by A60, NATTRA_1:def 5 ;
A72: F2 /. fi = FF2 . (f,(id c)) by A68, CAT_3:def 10
.= (curry (F2,f)) . (id c) by FUNCT_5:69
.= (F2 ?- f) . c by A70, FUNCT_2:15
.= T24 . c by A58, NATTRA_1:def 5 ;
A73: Hom ((F1 . [a,c]),(F1 . [b,c])) <> {} by A68, CAT_1:84;
thus (T34 `*` T13) . c = (T34 . c) * (T13 . c) by A59, A48, NATTRA_1:25
.= (t . [b,c]) (*) (F1 /. fi) by A63, A71, A65, CAT_1:def 13
.= (t . [b,c]) * (F1 /. fi) by A62, A73, CAT_1:def 13
.= (F2 /. fi) * (t . [a,c]) by A1, A68, NATTRA_1:def 8
.= (F2 /. fi) (*) (t . [a,c]) by A61, A69, CAT_1:def 13
.= (T24 . c) * (T12 . c) by A64, A72, A66, CAT_1:def 13
.= (T24 `*` T12) . c by A52, A57, NATTRA_1:25 ; :: thesis:

end;

then A74: T34 `*` T13 = T24 `*` T12 by A53, A58, NATTRA_1:18, NATTRA_1:19;
F1 ?- (dom f) = (export F1) . a by A40, A43, CAT_1:5;
then A75: (export F1) . g = [[S1,S3],T13] by A50, Def4;
Hom (((export F1) . b),((export F2) . b)) <> {} by A34;
hence (G . b) * ((export F1) /. f) = (G . b) (*) ((export F1) /. f) by A56, CAT_1:def 13
.= (G . b) (*) ((export F1) . g) by A40, CAT_3:def 10
.= [[S1,S4],(T34 `*` T13)] by A75, A51, NATTRA_1:36
.= ((export F2) /. g) (*) (G . a) by A55, A46, A74, NATTRA_1:36
.= ((export F2) /. f) (*) (G . a) by A40, CAT_3:def 10
.= ((export F2) /. f) * (G . a) by A54, A41, CAT_1:def 13 ;
:: thesis:

end;

A76: export F1 is_transformable_to export F2 by A37;
hence export F1 is_naturally_transformable_to export F2 by A39; :: thesis:
export F1 is_naturally_transformable_to export F2 by A39, A76;
then reconsider G = G as natural_transformation of export F1, export F2 by A39, NATTRA_1:def 8;
take G ; :: thesis:
let s be Function of [: the carrier of A, the carrier of B:], the carrier' of C; :: thesis:
assume A77: t = s ; :: thesis:
let a be Object of A; :: thesis:
thus G . a = G . a by A38, NATTRA_1:def 5
.= [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A33, A77 ; :: thesis: