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 & F2 is_naturally_transformable_to F3 ) and
A2: G1 is_naturally_transformable_to G2 and
A3: G2 is_naturally_transformable_to G3 ; :: thesis: (s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
A4: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 & F2 is_transformable_to F3 & G2 is_transformable_to G3 ) by A1, A2, A3, FUNCTOR2:def 6;
then A5: F1 is_transformable_to F3 by FUNCTOR2:4;
A6: ( G3 * F2 is_transformable_to G3 * F3 & G3 * F1 is_transformable_to G3 * F2 ) by A4, Th10;
G1 is_transformable_to G3 by A4, FUNCTOR2:4;
then A7: ( G1 * F1 is_transformable_to G3 * F1 & G1 * F1 is_transformable_to G2 * F1 & G2 * F1 is_transformable_to G3 * F1 ) by A4, Th10;
A8: ( G2 * F2 is_transformable_to G3 * F2 & G2 * F1 is_transformable_to G2 * F2 ) by A4, Th10;
G1 * F1 is_naturally_transformable_to G2 * F2 by A1, A2, Lm2;
then A9: G1 * F1 is_transformable_to G2 * F2 by FUNCTOR2:def 6;
A10: ( s1 (#) t1 = (G3 * t1) `*` (s1 * F2) & s (#) t = (G2 * t) `*` (s * F1) ) by A2, A3, A4, Th22;
thus (s1 `*` s) (#) (t1 `*` t) = (G3 * (t1 `*` t)) `*` ((s1 `*` s) * F1) by A2, A3, A5, Th22, FUNCTOR2:10
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by A4, Th13
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 `*` s) * F1) by A2, A3, FUNCTOR2:def 8
.= ((G3 * t1) `*` (G3 * t)) `*` ((s1 * F1) `*` (s * F1)) by A4, Th14
.= (G3 * t1) `*` ((G3 * t) `*` ((s1 * F1) `*` (s * F1))) by A6, A7, FUNCTOR2:8
.= (G3 * t1) `*` (((G3 * t) `*` (s1 * F1)) `*` (s * F1)) by A6, A7, FUNCTOR2:8
.= (G3 * t1) `*` ((s1 (#) t) `*` (s * F1)) by A3, A4, Th22
.= (G3 * t1) `*` ((s1 * F2) `*` ((G2 * t) `*` (s * F1))) by A7, A8, FUNCTOR2:8
.= (s1 (#) t1) `*` (s (#) t) by A6, A8, A9, A10, FUNCTOR2:8 ; :: thesis: verum