let A, B, C be category; for F1, F2, F3 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let F1, F2, F3 be covariant Functor of A,B; for G1, G2, G3 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let G1, G2, G3 be covariant Functor of B,C; for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let s be natural_transformation of G1,G2; for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let s1 be natural_transformation of G2,G3; for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let t be transformation of F1,F2; for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
let t1 be transformation of F2,F3; ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t) )
assume that
A1:
F1 is_naturally_transformable_to F2
and
A2:
F2 is_naturally_transformable_to F3
and
A3:
G1 is_naturally_transformable_to G2
and
A4:
G2 is_naturally_transformable_to G3
; (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
A5:
F1 is_transformable_to F2
by A1;
then A6:
s (#) t = (G2 * t) `*` (s * F1)
by A3, Th22;
A7:
G2 * F1 is_transformable_to G2 * F2
by A5, Th10;
A8:
G3 * F1 is_transformable_to G3 * F2
by A5, Th10;
G1 * F1 is_naturally_transformable_to G2 * F2
by A1, A3, Lm2;
then A9:
G1 * F1 is_transformable_to G2 * F2
;
A10:
G1 is_transformable_to G2
by A3;
then A11:
G1 * F1 is_transformable_to G2 * F1
by Th10;
A12:
F2 is_transformable_to F3
by A2;
then A13:
s1 (#) t1 = (G3 * t1) `*` (s1 * F2)
by A4, Th22;
A14:
G3 * F2 is_transformable_to G3 * F3
by A12, Th10;
A15:
G2 is_transformable_to G3
by A4;
then A16:
G2 * F1 is_transformable_to G3 * F1
by Th10;
G1 is_transformable_to G3
by A10, A15, FUNCTOR2:2;
then A17:
G1 * F1 is_transformable_to G3 * F1
by Th10;
A18:
G2 * F2 is_transformable_to G3 * F2
by A15, Th10;
F1 is_transformable_to F3
by A5, A12, FUNCTOR2:2;
hence (s1 `*` s) (#) (t1 `*` t) =
(G3 * (t1 `*` t)) `*` ((s1 `*` s) * F1)
by A3, A4, Th22, FUNCTOR2:8
.=
((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1)
by A5, A12, Th13
.=
((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1)
by A3, A4, FUNCTOR2:def 8
.=
((G3 * t1) `*` (G3 * t)) `*` ((s1 * F1) `*` (s * F1))
by A10, A15, Th14
.=
(G3 * t1) `*` ((G3 * t) `*` ((s1 * F1) `*` (s * F1)))
by A14, A8, A17, FUNCTOR2:6
.=
(G3 * t1) `*` (((G3 * t) `*` (s1 * F1)) `*` (s * F1))
by A8, A11, A16, FUNCTOR2:6
.=
(G3 * t1) `*` ((s1 (#) t) `*` (s * F1))
by A4, A5, Th22
.=
(G3 * t1) `*` ((s1 * F2) `*` ((G2 * t) `*` (s * F1)))
by A11, A18, A7, FUNCTOR2:6
.=
(s1 (#) t1) `*` (s (#) t)
by A14, A18, A9, A13, A6, FUNCTOR2:6
;
verum