let A, B, C be Category; for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)
let F1, F2, F3 be Functor of [:A,B:],C; ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1) )
assume that
A1:
F1 is_naturally_transformable_to F2
and
A2:
F2 is_naturally_transformable_to F3
; for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)
A3:
F2 is_transformable_to F3
by A2, NATTRA_1:def 7;
let t1 be natural_transformation of F1,F2; for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)
let t2 be natural_transformation of F2,F3; export (t2 `*` t1) = (export t2) `*` (export t1)
A4:
F1 is_transformable_to F2
by A1, NATTRA_1:def 7;
A5:
export F1 is_naturally_transformable_to export F2
by A1, Th27;
then A6:
export F1 is_transformable_to export F2
by NATTRA_1:def 7;
A7:
export F2 is_naturally_transformable_to export F3
by A2, Th27;
then A8:
export F2 is_transformable_to export F3
by NATTRA_1:def 7;
A9:
F1 is_naturally_transformable_to F3
by A1, A2, NATTRA_1:25;
then A10:
F1 is_transformable_to F3
by NATTRA_1:def 7;
now let a be
Object of
A;
(export (t2 `*` t1)) . a = ((export t2) `*` (export t1)) . areconsider S1 =
(export F1) . a,
S2 =
(export F2) . a,
S3 =
(export F3) . a as
Functor of
B,
C by Th8;
the
carrier of
[:A,B:] = [:the carrier of A,the carrier of B:]
by CAT_2:33;
then reconsider s1 =
t1,
s2 =
t2,
s3 =
t2 `*` t1 as
Function of
[:the carrier of A,the carrier of B:],the
carrier' of
C ;
A11:
S2 = F2 ?- a
by Th24;
A12:
S3 = F3 ?- a
by Th24;
then reconsider T2 =
(curry s2) . a as
natural_transformation of
S2,
S3 by A2, A11, Th15;
A13:
S2 is_naturally_transformable_to S3
by A2, A11, A12, Th15;
then A14:
S2 is_transformable_to S3
by NATTRA_1:def 7;
A15:
S1 = F1 ?- a
by Th24;
then reconsider T1 =
(curry s1) . a as
natural_transformation of
S1,
S2 by A1, A11, Th15;
A16:
(
(export t2) . a = [[S2,S3],T2] &
(export t1) . a = [[S1,S2],T1] )
by A1, A2, Def5;
A17:
S1 is_naturally_transformable_to S2
by A1, A15, A11, Th15;
then
S1 is_naturally_transformable_to S3
by A13, NATTRA_1:25;
then A18:
S1 is_transformable_to S3
by NATTRA_1:def 7;
reconsider T3 =
(curry s3) . a as
natural_transformation of
S1,
S3 by A9, A15, A12, Th15;
A19:
(
Hom ((export F1) . a),
((export F2) . a) <> {} &
Hom ((export F2) . a),
((export F3) . a) <> {} )
by A6, A8, NATTRA_1:def 2;
A20:
S1 is_transformable_to S2
by A17, NATTRA_1:def 7;
now let b be
Object of
B;
T3 . b = (T2 `*` T1) . bA21:
(
Hom (F1 . [a,b]),
(F2 . [a,b]) <> {} &
Hom (F2 . [a,b]),
(F3 . [a,b]) <> {} )
by A4, A3, NATTRA_1:def 2;
A22:
(
Hom (S1 . b),
(S2 . b) <> {} &
Hom (S2 . b),
(S3 . b) <> {} )
by A20, A14, NATTRA_1:def 2;
A23:
T1 . b =
T1 . b
by A20, NATTRA_1:def 5
.=
s1 . a,
b
by CAT_2:3
.=
t1 . [a,b]
by A4, NATTRA_1:def 5
;
A24:
T2 . b =
T2 . b
by A14, NATTRA_1:def 5
.=
s2 . a,
b
by CAT_2:3
.=
t2 . [a,b]
by A3, NATTRA_1:def 5
;
thus T3 . b =
T3 . b
by A18, NATTRA_1:def 5
.=
s3 . a,
b
by CAT_2:3
.=
(t2 `*` t1) . [a,b]
by A10, NATTRA_1:def 5
.=
(t2 . [a,b]) * (t1 . [a,b])
by A1, A2, NATTRA_1:27
.=
(T2 . b) * (T1 . b)
by A21, A24, A23, CAT_1:def 13
.=
(T2 . b) * (T1 . b)
by A22, CAT_1:def 13
.=
(T2 `*` T1) . b
by A17, A13, NATTRA_1:27
;
verum end; then A25:
T3 = T2 `*` T1
by A18, NATTRA_1:20;
thus (export (t2 `*` t1)) . a =
[[S1,S3],T3]
by A9, Def5
.=
((export t2) . a) * ((export t1) . a)
by A16, A25, NATTRA_1:42
.=
((export t2) . a) * ((export t1) . a)
by A19, CAT_1:def 13
.=
((export t2) `*` (export t1)) . a
by A5, A7, NATTRA_1:27
;
verum end;
hence
export (t2 `*` t1) = (export t2) `*` (export t1)
by A6, A8, NATTRA_1:19, NATTRA_1:20; verum