let A, B, C be category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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 ;
A7: G2 * F1 is_transformable_to G2 * F2 by ;
A8: G3 * F1 is_transformable_to G3 * F2 by ;
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 ;
A14: G3 * F2 is_transformable_to G3 * F3 by ;
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 ;
then A17: G1 * F1 is_transformable_to G3 * F1 by Th10;
A18: G2 * F2 is_transformable_to G3 * F2 by ;
F1 is_transformable_to F3 by ;
hence (s1 `*` s) (#) (t1 `*` t) = (G3 * (t1 `*` t)) `*` ((s1 `*` s) * F1) by
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 * F1) `*` (s * F1)) by
.= (G3 * t1) `*` ((G3 * t) `*` ((s1 * F1) `*` (s * F1))) by
.= (G3 * t1) `*` (((G3 * t) `*` (s1 * F1)) `*` (s * F1)) by
.= (G3 * t1) `*` ((s1 (#) t) `*` (s * F1)) by A4, A5, Th22
.= (G3 * t1) `*` ((s1 * F2) `*` ((G2 * t) `*` (s * F1))) by
.= (s1 (#) t1) `*` (s (#) t) by ;
:: thesis: verum