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 s' being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t' 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
(t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (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 s' being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t' 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
(t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (t (#) s)
let G1, G2, G3 be Functor of B,C; :: thesis: for s being natural_transformation of F1,F2
for s' being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t' 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
(t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (t (#) s)
let s be natural_transformation of F1,F2; :: thesis: for s' being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t' 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
(t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (t (#) s)
let s' be natural_transformation of F2,F3; :: thesis: for t being natural_transformation of G1,G2
for t' 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
(t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (t (#) s)
let t be natural_transformation of G1,G2; :: thesis: for t' 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
(t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (t (#) s)
let t' 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 (t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (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: (t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (t (#) s)
A5: ( t' (#) s' = (G3 * s') `*` (t' * F2) & t (#) s = (G2 * s) `*` (t * F1) ) by A1, A2, A3, A4, Th41;
A6: G1 * F1 is_naturally_transformable_to G2 * F1 by A3, Th27;
A7: G2 * F1 is_naturally_transformable_to G2 * F2 by A1, Th27;
then A8: G1 * F1 is_naturally_transformable_to G2 * F2 by A6, NATTRA_1:25;
A9: G2 * F2 is_naturally_transformable_to G3 * F2 by A4, Th27;
A10: G1 is_naturally_transformable_to G3 by A3, A4, NATTRA_1:25;
then A11: G1 * F1 is_naturally_transformable_to G3 * F1 by Th27;
A12: G3 * F1 is_naturally_transformable_to G3 * F2 by A1, Th27;
A13: G2 * F1 is_naturally_transformable_to G3 * F1 by A4, Th27;
A14: G3 * F2 is_naturally_transformable_to G3 * F3 by A2, Th27;
F1 is_naturally_transformable_to F3 by A1, A2, NATTRA_1:25;
hence (t' `*` t) (#) (s' `*` s) = (G3 * (s' `*` s)) `*` ((t' `*` t) * F1) by A10, Th41
.= ((G3 * s') `*` (G3 * s)) `*` ((t' `*` t) * F1) by A1, A2, Th32
.= ((G3 * s') `*` (G3 * s)) `*` ((t' * F1) `*` (t * F1)) by A3, A4, Th33
.= (G3 * s') `*` ((G3 * s) `*` ((t' * F1) `*` (t * F1))) by A14, A12, A11, NATTRA_1:28
.= (G3 * s') `*` (((G3 * s) `*` (t' * F1)) `*` (t * F1)) by A12, A6, A13, NATTRA_1:28
.= (G3 * s') `*` ((t' (#) s) `*` (t * F1)) by A1, A4, Th41
.= (G3 * s') `*` ((t' * F2) `*` ((G2 * s) `*` (t * F1))) by A6, A9, A7, NATTRA_1:28
.= (t' (#) s') `*` (t (#) s) by A14, A9, A8, A5, NATTRA_1:28 ;
:: thesis: verum