let A, B, C be Category; 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; ( 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
; 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; 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; ( 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
A4:
now let b be
Object of
B;
((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;
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;
( 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 <> {}
;
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;
(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
;
verum end;
hence
F1 ?- a is_naturally_transformable_to F2 ?- a
by A3, NATTRA_1:def 7; (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; verum