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 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 ;
:: thesis: verum