let A, B, C be Category; :: thesis: for F1, F2, F3 being Functor of A,B
for G1, G2, G3 being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 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
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let F1, F2, F3 be Functor of A,B; :: thesis: for G1, G2, G3 being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 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
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let G1, G2, G3 be Functor of B,C; :: thesis: for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 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
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let s be natural_transformation of F1,F2; :: thesis: for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 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
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let s9 be natural_transformation of F2,F3; :: thesis: for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 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
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let t be natural_transformation of G1,G2; :: thesis: for t9 being natural_transformation of G2,G3 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
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let t9 be natural_transformation of G2,G3; :: 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 (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) )
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: (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
A5: ( t9 (#) s9 = (G3 * s9) `*` (t9 * F2) & t (#) s = (G2 * s) `*` (t * F1) ) by A1, A2, A3, A4, Th34;
A6: G1 * F1 is_naturally_transformable_to G2 * F1 by A3, Th20;
A7: G2 * F1 is_naturally_transformable_to G2 * F2 by A1, Th20;
then A8: G1 * F1 is_naturally_transformable_to G2 * F2 by A6, NATTRA_1:23;
A9: G2 * F2 is_naturally_transformable_to G3 * F2 by A4, Th20;
A10: G1 is_naturally_transformable_to G3 by A3, A4, NATTRA_1:23;
then A11: G1 * F1 is_naturally_transformable_to G3 * F1 by Th20;
A12: G3 * F1 is_naturally_transformable_to G3 * F2 by A1, Th20;
A13: G2 * F1 is_naturally_transformable_to G3 * F1 by A4, Th20;
A14: G3 * F2 is_naturally_transformable_to G3 * F3 by A2, Th20;
F1 is_naturally_transformable_to F3 by A1, A2, NATTRA_1:23;
hence (t9 `*` t) (#) (s9 `*` s) = (G3 * (s9 `*` s)) `*` ((t9 `*` t) * F1) by A10, Th34
.= ((G3 * s9) `*` (G3 * s)) `*` ((t9 `*` t) * F1) by A1, A2, Th25
.= ((G3 * s9) `*` (G3 * s)) `*` ((t9 * F1) `*` (t * F1)) by A3, A4, Th26
.= (G3 * s9) `*` ((G3 * s) `*` ((t9 * F1) `*` (t * F1))) by A14, A12, A11, NATTRA_1:26
.= (G3 * s9) `*` (((G3 * s) `*` (t9 * F1)) `*` (t * F1)) by A12, A6, A13, NATTRA_1:26
.= (G3 * s9) `*` ((t9 (#) s) `*` (t * F1)) by A1, A4, Th34
.= (G3 * s9) `*` ((t9 * F2) `*` ((G2 * s) `*` (t * F1))) by A6, A9, A7, NATTRA_1:26
.= (t9 (#) s9) `*` (t (#) s) by A14, A9, A8, A5, NATTRA_1:26 ;
:: thesis: verum