let A, B, C be Category; for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds
t1 = t2
let F1, F2 be Functor of [:A,B:],C; ( F1 is_naturally_transformable_to F2 implies for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds
t1 = t2 )
assume A1:
F1 is_naturally_transformable_to F2
; for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds
t1 = t2
then A2:
F1 is_transformable_to F2
;
let t1, t2 be natural_transformation of F1,F2; ( export t1 = export t2 implies t1 = t2 )
assume A3:
export t1 = export t2
; t1 = t2
now for ab being Object of [:A,B:] holds t1 . ab = t2 . abreconsider s1 =
t1,
s2 =
t2 as
Function of
[: the carrier of A, the carrier of B:], the
carrier' of
C ;
let ab be
Object of
[:A,B:];
t1 . ab = t2 . abconsider a being
Object of
A,
b being
Object of
B such that A4:
ab = [a,b]
by DOMAIN_1:1;
[[((export F1) . a),((export F2) . a)],((curry s1) . a)] =
(export t1) . a
by A1, Def5
.=
[[((export F1) . a),((export F2) . a)],((curry s2) . a)]
by A1, A3, Def5
;
then A5:
(curry s1) . a = (curry s2) . a
by XTUPLE_0:1;
thus t1 . ab =
s1 . (
a,
b)
by A2, A4, NATTRA_1:def 5
.=
((curry s2) . a) . b
by A5, FUNCT_5:69
.=
s2 . (
a,
b)
by FUNCT_5:69
.=
t2 . ab
by A2, A4, NATTRA_1:def 5
;
verum end;
hence
t1 = t2
by A1, ISOCAT_1:26; verum