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
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- 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
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a ) )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )
then A2: F1 is_transformable_to F2 by NATTRA_1:def 7;
let u be natural_transformation of F1,F2; :: thesis: for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a )
let a be Object of A; :: thesis: ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a )
the carrier of [:A,B:] = [: the carrier of A, the carrier of B:] by CAT_2:33;
then reconsider t = u as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
A3: F1 ?- a is_transformable_to F2 ?- a

proof

let b be Object of B; :: according to NATTRA_1:def 2 :: thesis: not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {}
( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th12;
hence not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {} by A2, NATTRA_1:def 2; :: thesis: verum

end;

A4: now

let b be Object of B; :: thesis: ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b))
A5: ( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th12;
A6: Hom (((F1 ?- a) . b),((F2 ?- a) . b)) <> {} by A3, NATTRA_1:def 2;
((curry t) . a) . b = t . (a,b) by CAT_2:3
.= u . [a,b] by A2, NATTRA_1:def 5 ;
hence ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A5, A6, CAT_1:def 7; :: thesis: verum

end;

now

let b be Object of B; :: thesis: ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b
((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A4;
hence ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b by CAT_1:def 7; :: thesis: verum

end;

then reconsider s = (curry t) . a as transformation of F1 ?- a,F2 ?- a by A3, NATTRA_1:def 3;

A7: now

let b1, b2 be Object of B; :: thesis: ( Hom (b1,b2) <> {} implies for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) . f) = ((F2 ?- a) . f) * (s . b1) )
assume A8: Hom (b1,b2) <> {} ; :: thesis: for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) . f) = ((F2 ?- a) . f) * (s . b1)
A9: Hom (((F1 ?- a) . b1),((F1 ?- a) . b2)) <> {} by A8, CAT_1:126;
let f be Morphism of b1,b2; :: thesis: (s . b2) * ((F1 ?- a) . f) = ((F2 ?- a) . f) * (s . b1)
A10: Hom (a,a) <> {} by CAT_1:56;
then reconsider g = [(id a),f] as Morphism of [a,b1],[a,b2] by A8, CAT_2:43;
A11: Hom ([a,b1],[a,b2]) <> {} by A8, A10, Th13;
then A12: Hom ((F1 . [a,b1]),(F1 . [a,b2])) <> {} by CAT_1:126;
A13: s . b1 = ((curry t) . a) . b1 by A3, NATTRA_1:def 5
.= t . (a,b1) by CAT_2:3
.= u . [a,b1] by A2, NATTRA_1:def 5 ;
A14: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2, NATTRA_1:def 2;
A15: Hom (((F2 ?- a) . b1),((F2 ?- a) . b2)) <> {} by A8, CAT_1:126;
A16: ( (F1 ?- a) . b1 = F1 . [a,b1] & (F2 ?- a) . b1 = F2 . [a,b1] ) by Th12;
A17: ( (F1 ?- a) . b2 = F1 . [a,b2] & (F2 ?- a) . b2 = F2 . [a,b2] ) by Th12;
A18: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2, NATTRA_1:def 2;
A19: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A11, CAT_1:126;
s . b2 = ((curry t) . a) . b2 by A3, NATTRA_1:def 5
.= t . (a,b2) by CAT_2:3
.= u . [a,b2] by A2, NATTRA_1:def 5 ;
hence (s . b2) * ((F1 ?- a) . f) = (u . [a,b2]) * ((F1 ?- a) . f) by A14, A9, A17, CAT_1:def 13
.= (u . [a,b2]) * ((F1 ?- a) . f) by A8, NATTRA_1:def 1
.= (u . [a,b2]) * (F1 . ((id a),f)) by CAT_2:47
.= (u . [a,b2]) * (F1 . g) by A11, NATTRA_1:def 1
.= (u . [a,b2]) * (F1 . g) by A12, A14, CAT_1:def 13
.= (F2 . g) * (u . [a,b1]) by A1, A11, NATTRA_1:def 8
.= (F2 . g) * (u . [a,b1]) by A18, A19, CAT_1:def 13
.= (F2 . ((id a),f)) * (u . [a,b1]) by A11, NATTRA_1:def 1
.= ((F2 ?- a) . f) * (u . [a,b1]) by CAT_2:47
.= ((F2 ?- a) . f) * (s . b1) by A8, A13, NATTRA_1:def 1
.= ((F2 ?- a) . f) * (s . b1) by A18, A15, A16, CAT_1:def 13 ;
:: thesis: verum

end;

hence F1 ?- a is_naturally_transformable_to F2 ?- a by A3, NATTRA_1:def 7; :: thesis: (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a
hence (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a by A7, NATTRA_1:def 8; :: thesis: verum