let A, B be category; for F, F1, F2, F3 being covariant Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let F, F1, F2, F3 be covariant Functor of A,B; for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let t be natural_transformation of F,F1; for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let t1 be natural_transformation of F1,F2; ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) )
assume that
A1:
F is_naturally_transformable_to F1
and
A2:
F1 is_naturally_transformable_to F2
and
A3:
F2 is_naturally_transformable_to F3
; for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
A4:
F is_naturally_transformable_to F2
by A1, A2, Th8;
let t3 be natural_transformation of F2,F3; (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
A5:
F2 is_transformable_to F3
by A3;
A6:
( F is_transformable_to F1 & F1 is_transformable_to F2 )
by A1, A2;
F1 is_naturally_transformable_to F3
by A2, A3, Th8;
hence (t3 `*` t1) `*` t =
(t3 `*` t1) `*` t
by A1, Def8
.=
(t3 `*` t1) `*` t
by A2, A3, Def8
.=
t3 `*` (t1 `*` t)
by A6, A5, Th6
.=
t3 `*` (t1 `*` t)
by A1, A2, Def8
.=
t3 `*` (t1 `*` t)
by A3, A4, Def8
;
verum