let A, B, C be Category; :: thesis: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
let F1, F2 be Functor of [:A,B:],C; :: thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds
( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: for t being natural_transformation of F1,F2 holds
( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
then A2: F1 is_transformable_to F2 by NATTRA_1:def 7;
let t be natural_transformation of F1,F2; :: thesis: ( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
the carrier of [:A,B:] = [: the carrier of A, the carrier of B:] by CAT_2:23;
then reconsider s = t as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;

A3: now

let a be Object of A; :: thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds
for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b))
let S1, S2 be Functor of B,C; :: thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) )
assume that
A4: S1 = (export F1) . a and
A5: S2 = (export F2) . a ; :: thesis: for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b))
let b be Object of B; :: thesis: ((curry s) . a) . b in Hom ((S1 . b),(S2 . b))
A6: S2 . b = (F2 ?- a) . b by A5, Th24
.= F2 . [a,b] by Th12 ;
A7: ((curry s) . a) . b = s . (a,b) by CAT_2:3
.= t . [a,b] by A2, NATTRA_1:def 5 ;
S1 . b = (F1 ?- a) . b by A4, Th24
.= F1 . [a,b] by Th12 ;
hence ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A2, A6, A7, Lm1; :: thesis: verum

end;

A8: now

let a be Object of A; :: thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds
S1 is_transformable_to S2
let S1, S2 be Functor of B,C; :: thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies S1 is_transformable_to S2 )
assume ( S1 = (export F1) . a & S2 = (export F2) . a ) ; :: thesis: S1 is_transformable_to S2
then for b being Object of B holds Hom ((S1 . b),(S2 . b)) <> {} by A3;
hence S1 is_transformable_to S2 by NATTRA_1:def 2; :: thesis: verum

end;

A9: now

let a be Object of A; :: thesis: for S1, S2 being Functor of B,C
for T being transformation of S1,S2 st S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a holds
for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 . f) = (S2 . f) * (T . b1)
let S1, S2 be Functor of B,C; :: thesis: for T being transformation of S1,S2 st S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a holds
for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 . f) = (S2 . f) * (T . b1)
let T be transformation of S1,S2; :: thesis: ( S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a implies for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 . f) = (S2 . f) * (T . b1) )
assume that
A10: S1 = (export F1) . a and
A11: S2 = (export F2) . a and
A12: T = (curry s) . a ; :: thesis: for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 . f) = (S2 . f) * (T . b1)
let b1, b2 be Object of B; :: thesis: ( Hom (b1,b2) <> {} implies for f being Morphism of b1,b2 holds (T . b2) * (S1 . f) = (S2 . f) * (T . b1) )
assume A13: Hom (b1,b2) <> {} ; :: thesis: for f being Morphism of b1,b2 holds (T . b2) * (S1 . f) = (S2 . f) * (T . b1)
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, CAT_2:3
.= t . [a,b2] by A2, NATTRA_1:def 5 ;
A16: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2, NATTRA_1:def 2;
let f be Morphism of b1,b2; :: thesis: (T . b2) * (S1 . f) = (S2 . f) * (T . b1)
A17: Hom (a,a) <> {} by CAT_1:27;
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, Th13;
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)) <> {} by NATTRA_1:def 2;
A22: T . b1 = T . b1 by A8, A10, A11, NATTRA_1:def 5
.= s . (a,b1) by A12, CAT_2:3
.= t . [a,b1] by A2, NATTRA_1:def 5 ;
A23: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2, NATTRA_1:def 2;
A24: Hom ((S1 . b2),(S2 . b2)) <> {} by A20, NATTRA_1:def 2;
A25: Hom ((S2 . b1),(S2 . b2)) <> {} by A13, CAT_1:84;
A26: S2 . f = (F2 ?- a) . f by A11, Th24
.= (F2 ?- a) . f by A13, NATTRA_1:def 1
.= F2 . ((id a),f) by CAT_2:36
.= F2 . g by A18, NATTRA_1:def 1 ;
A27: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A18, CAT_1:84;
S1 . f = (F1 ?- a) . f by A10, Th24
.= (F1 ?- a) . f by A13, NATTRA_1:def 1
.= F1 . ((id a),f) by CAT_2:36
.= F1 . g by A18, NATTRA_1:def 1 ;
hence (T . b2) * (S1 . f) = (t . [a,b2]) * (F1 . g) by A14, A24, A15, CAT_1:def 10
.= (t . [a,b2]) * (F1 . g) by A19, A16, CAT_1:def 10
.= (F2 . g) * (t . [a,b1]) by A1, A18, NATTRA_1:def 8
.= (S2 . f) * (T . b1) by A27, A23, A22, A26, CAT_1:def 10
.= (S2 . f) * (T . b1) by A25, A21, CAT_1:def 10 ;
:: thesis: verum

end;

defpred S₁[ set , set ] 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)];

A28: now

let a be Object of A; :: thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds
(curry s) . a is transformation of S1,S2
let S1, S2 be Functor of B,C; :: thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies (curry s) . a is transformation of S1,S2 )
assume A29: ( S1 = (export F1) . a & S2 = (export F2) . a ) ; :: thesis: (curry s) . a is transformation of S1,S2
thus (curry s) . a is transformation of S1,S2 :: thesis: verum

proof

thus S1 is_transformable_to S2 by A8, A29; :: according to NATTRA_1:def 3 :: thesis: for b₁ being Element of the carrier of B holds ((curry s) . a) . b₁ is Morphism of S1 . b₁,S2 . b₁
let b be Object of B; :: thesis: ((curry s) . a) . b is Morphism of S1 . b,S2 . b
((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A3, A29;
hence ((curry s) . a) . b is Morphism of S1 . b,S2 . b by CAT_1:def 4; :: thesis: verum

end;

end;

A30: now

let m be set ; :: thesis: ( m in the carrier of A implies ex o being set st
( o in the carrier' of (Functors (B,C)) & S₁[m,o] ) )
assume m in the carrier of A ; :: thesis: ex o being set st
( o in the carrier' of (Functors (B,C)) & S₁[m,o] )
then reconsider a = m as Object of A ;
reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th25;
take o = [[((export F1) . a),((export F2) . a)],((curry s) . a)]; :: thesis: ( o in the carrier' of (Functors (B,C)) & S₁[m,o] )
reconsider T = (curry s) . a as transformation of S1,S2 by A28;
A31: S1 is_naturally_transformable_to S2

proof

thus S1 is_transformable_to S2 by A8; :: according to NATTRA_1:def 7 :: thesis: ex b₁ being transformation of S1,S2 st
for b₂, b₃ being Element of the carrier of B holds
( Hom (b₂,b₃) = {} or for b₄ being Morphism of b₂,b₃ holds (b₁ . b₃) * (S1 . b₄) = (S2 . b₄) * (b₁ . b₂) )
take T ; :: thesis: 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₁) )
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: verum

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 A31, NATTRA_1:def 8;
then o in NatTrans (B,C) by A31, NATTRA_1:32;
hence o in the carrier' of (Functors (B,C)) by NATTRA_1:def 17; :: thesis: S₁[m,o]
thus S₁[m,o] ; :: thesis: verum

end;

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

A33: now

let a be Object of A; :: thesis: G . a in Hom (((export F1) . a),((export F2) . a))
reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th25;
reconsider T = (curry s) . a as transformation of S1,S2 by A28;
A34: G . a = [[S1,S2],T] by A32;
A35: S1 is_naturally_transformable_to S2

proof

thus S1 is_transformable_to S2 by A8; :: according to NATTRA_1:def 7 :: thesis: ex b₁ being transformation of S1,S2 st
for b₂, b₃ being Element of the carrier of B holds
( Hom (b₂,b₃) = {} or for b₄ being Morphism of b₂,b₃ holds (b₁ . b₃) * (S1 . b₄) = (S2 . b₄) * (b₁ . b₂) )
take T ; :: thesis: 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₁) )
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: verum

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 A35, NATTRA_1:def 8;
then ( dom (G . a) = S1 & cod (G . a) = S2 ) by A34, NATTRA_1:33;
hence G . a in Hom (((export F1) . a),((export F2) . a)) ; :: thesis: verum

end;

then A36: 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 A36, NATTRA_1:def 2; :: according to NATTRA_1:def 3 :: thesis: for b₁ being Element of the carrier of A holds G . b₁ is Morphism of (export F1) . b₁,(export F2) . b₁
let a be Object of A; :: thesis: G . a is Morphism of (export F1) . a,(export F2) . a
G . a in Hom (((export F1) . a),((export F2) . a)) by A33;
hence G . a is Morphism of (export F1) . a,(export F2) . a by CAT_1:def 4; :: thesis: verum

end;

then reconsider G = G as transformation of export F1, export F2 ;
A37: export F1 is_transformable_to export F2 by A36, NATTRA_1:def 2;

A38: now

let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (G . b) * ((export F1) . f) = ((export F2) . f) * (G . a) )
assume A39: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds (G . b) * ((export F1) . f) = ((export F2) . f) * (G . a)
A40: Hom (((export F2) . a),((export F2) . b)) <> {} by A39, 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 Th25;
let f be Morphism of a,b; :: thesis: (G . b) * ((export F1) . f) = ((export F2) . f) * (G . a)
A41: F2 ?- a = (export F2) . a by Th24;
A42: F1 ?- a = (export F1) . a by Th24;
then reconsider T12 = (curry s) . a as natural_transformation of S1,S2 by A1, A41, Th15;
A43: F2 ?- b = (export F2) . b by Th24;
then A44: F2 ?- (cod f) = (export F2) . b by A39, CAT_1:5;
then reconsider T24 = F2 ?- f as natural_transformation of S2,S4 by A39, A41, CAT_1:5;
A45: G . a = G . a by A37, NATTRA_1:def 5
.= [[S1,S2],T12] by A32 ;
A46: F1 ?- b = (export F1) . b by Th24;
then reconsider T34 = (curry s) . b as natural_transformation of S3,S4 by A1, A43, Th15;
A47: S3 is_naturally_transformable_to S4 by A1, A46, A43, Th15;
then A48: S3 is_transformable_to S4 by NATTRA_1:def 7;
A49: F1 ?- (cod f) = (export F1) . b by A39, A46, CAT_1:5;
then reconsider T13 = F1 ?- f as natural_transformation of S1,S3 by A39, A42, CAT_1:5;
A50: G . b = G . b by A37, NATTRA_1:def 5
.= [[S3,S4],T34] by A32 ;
A51: S1 is_naturally_transformable_to S2 by A1, A41, A42, Th15;
then A52: S1 is_transformable_to S2 by NATTRA_1:def 7;
reconsider g = f as Morphism of A ;
A53: Hom (((export F1) . a),((export F2) . a)) <> {} by A33;
F2 ?- (dom f) = (export F2) . a by A39, A41, CAT_1:5;
then A54: (export F2) . g = [[S2,S4],T24] by A44, Def4;
A55: Hom (((export F1) . a),((export F1) . b)) <> {} by A39, CAT_1:84;
A56: S2 is_naturally_transformable_to S4 by A39, A41, A43, Th17;
then A57: S2 is_transformable_to S4 by NATTRA_1:def 7;
A58: S1 is_naturally_transformable_to S3 by A39, A46, A42, Th17;
then A59: S1 is_transformable_to S3 by NATTRA_1:def 7;

now

the carrier' of [:A,B:] = [: the carrier' of A, the carrier' of B:] by CAT_2:23;
then 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: (T34 `*` T13) . c = (T24 `*` T12) . c
A60: Hom ((F1 . [a,c]),(F2 . [a,c])) <> {} by A2, NATTRA_1:def 2;
A61: Hom ((F1 . [b,c]),(F2 . [b,c])) <> {} by A2, NATTRA_1:def 2;
A62: ( Hom ((S3 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S3 . c)) <> {} ) by A59, A48, NATTRA_1:def 2;
A63: ( Hom ((S2 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S2 . c)) <> {} ) by A52, A57, NATTRA_1:def 2;
A64: t . [b,c] = s . (b,c) by A2, NATTRA_1:def 5
.= ((curry s) . b) . c by CAT_2:3
.= T34 . c by A48, NATTRA_1:def 5 ;
A65: t . [a,c] = s . (a,c) by A2, NATTRA_1:def 5
.= ((curry s) . a) . c by CAT_2:3
.= T12 . c by A52, NATTRA_1:def 5 ;
A66: Hom (c,c) <> {} by CAT_1:27;
then reconsider fi = [f,(id c)] as Morphism of [a,c],[b,c] by A39, CAT_2:33;
A67: Hom ([a,c],[b,c]) <> {} by A39, A66, Th13;
then A68: Hom ((F2 . [a,c]),(F2 . [b,c])) <> {} by CAT_1:84;
A69: F1 . fi = FF1 . (f,(id c)) by A67, NATTRA_1:def 1
.= (curry (F1,f)) . (id c) by CAT_2:3
.= (F1 ?- f) . c by FUNCT_2:15
.= T13 . c by A59, NATTRA_1:def 5 ;
A70: F2 . fi = FF2 . (f,(id c)) by A67, NATTRA_1:def 1
.= (curry (F2,f)) . (id c) by CAT_2:3
.= (F2 ?- f) . c by FUNCT_2:15
.= T24 . c by A57, NATTRA_1:def 5 ;
A71: Hom ((F1 . [a,c]),(F1 . [b,c])) <> {} by A67, CAT_1:84;
thus (T34 `*` T13) . c = (T34 . c) * (T13 . c) by A58, A47, NATTRA_1:25
.= (t . [b,c]) * (F1 . fi) by A62, A69, A64, CAT_1:def 10
.= (t . [b,c]) * (F1 . fi) by A61, A71, CAT_1:def 10
.= (F2 . fi) * (t . [a,c]) by A1, A67, NATTRA_1:def 8
.= (F2 . fi) * (t . [a,c]) by A60, A68, CAT_1:def 10
.= (T24 . c) * (T12 . c) by A63, A70, A65, CAT_1:def 10
.= (T24 `*` T12) . c by A51, A56, NATTRA_1:25 ; :: thesis: verum

end;

then A72: T34 `*` T13 = T24 `*` T12 by A52, A57, NATTRA_1:18, NATTRA_1:19;
F1 ?- (dom f) = (export F1) . a by A39, A42, CAT_1:5;
then A73: (export F1) . g = [[S1,S3],T13] by A49, Def4;
Hom (((export F1) . b),((export F2) . b)) <> {} by A33;
hence (G . b) * ((export F1) . f) = (G . b) * ((export F1) . f) by A55, CAT_1:def 10
.= (G . b) * ((export F1) . g) by A39, NATTRA_1:def 1
.= [[S1,S4],(T34 `*` T13)] by A73, A50, NATTRA_1:36
.= ((export F2) . g) * (G . a) by A54, A45, A72, NATTRA_1:36
.= ((export F2) . f) * (G . a) by A39, NATTRA_1:def 1
.= ((export F2) . f) * (G . a) by A53, A40, CAT_1:def 10 ;
:: thesis: verum

end;

A74: export F1 is_transformable_to export F2 by A36, NATTRA_1:def 2;
hence export F1 is_naturally_transformable_to export F2 by A38, NATTRA_1:def 7; :: thesis: ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
export F1 is_naturally_transformable_to export F2 by A38, A74, NATTRA_1:def 7;
then reconsider G = G as natural_transformation of export F1, export F2 by A38, NATTRA_1:def 8;
take G ; :: thesis: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
let s be Function of [: the carrier of A, the carrier of B:], the carrier' of C; :: thesis: ( t = s implies for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
assume A75: t = s ; :: thesis: for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
let a be Object of A; :: thesis: G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
thus G . a = G . a by A37, NATTRA_1:def 5
.= [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A32, A75 ; :: thesis: verum