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;
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;
A5:
export F1 is_naturally_transformable_to export F2
by A1, Th21;
then A6:
export F1 is_transformable_to export F2
;
A7:
export F2 is_naturally_transformable_to export F3
by A2, Th21;
then A8:
export F2 is_transformable_to export F3
;
A9:
F1 is_naturally_transformable_to F3
by A1, A2, NATTRA_1:23;
then A10:
F1 is_transformable_to F3
;
now for a being Object of A holds (export (t2 `*` t1)) . a = ((export t2) `*` (export t1)) . alet 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 Th5;
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 Th18;
A12:
S3 = F3 ?- a
by Th18;
then reconsider T2 =
(curry s2) . a as
natural_transformation of
S2,
S3 by A2, A11, Th11;
A13:
S2 is_naturally_transformable_to S3
by A2, A11, A12, Th11;
then A14:
S2 is_transformable_to S3
;
A15:
S1 = F1 ?- a
by Th18;
then reconsider T1 =
(curry s1) . a as
natural_transformation of
S1,
S2 by A1, A11, Th11;
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, Th11;
then
S1 is_naturally_transformable_to S3
by A13, NATTRA_1:23;
then A18:
S1 is_transformable_to S3
;
reconsider T3 =
(curry s3) . a as
natural_transformation of
S1,
S3 by A9, A15, A12, Th11;
A19:
(
Hom (
((export F1) . a),
((export F2) . a))
<> {} &
Hom (
((export F2) . a),
((export F3) . a))
<> {} )
by A6, A8;
A20:
S1 is_transformable_to S2
by A17;
now for b being Object of B holds T3 . b = (T2 `*` T1) . blet 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;
A22:
(
Hom (
(S1 . b),
(S2 . b))
<> {} &
Hom (
(S2 . b),
(S3 . b))
<> {} )
by A20, A14;
A23:
T1 . b =
T1 . b
by A20, NATTRA_1:def 5
.=
s1 . (
a,
b)
by FUNCT_5:69
.=
t1 . [a,b]
by A4, NATTRA_1:def 5
;
A24:
T2 . b =
T2 . b
by A14, NATTRA_1:def 5
.=
s2 . (
a,
b)
by FUNCT_5:69
.=
t2 . [a,b]
by A3, NATTRA_1:def 5
;
thus T3 . b =
T3 . b
by A18, NATTRA_1:def 5
.=
s3 . (
a,
b)
by FUNCT_5:69
.=
(t2 `*` t1) . [a,b]
by A10, NATTRA_1:def 5
.=
(t2 . [a,b]) * (t1 . [a,b])
by A1, A2, NATTRA_1:25
.=
(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:25
;
verum end; then A25:
T3 = T2 `*` T1
by A18, NATTRA_1:19;
thus (export (t2 `*` t1)) . a =
[[S1,S3],T3]
by A9, Def5
.=
((export t2) . a) (*) ((export t1) . a)
by A16, A25, NATTRA_1:36
.=
((export t2) . a) * ((export t1) . a)
by A19, CAT_1:def 13
.=
((export t2) `*` (export t1)) . a
by A5, A7, NATTRA_1:25
;
verum end;
hence
export (t2 `*` t1) = (export t2) `*` (export t1)
by A6, A8, NATTRA_1:18, NATTRA_1:19; verum