let A, B, C, D be Category; :: thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let F1, F2 be Functor of A,B; :: thesis: for G1, G2 being Functor of B,C
for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let G1, G2 be Functor of B,C; :: thesis: for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let H1, H2 be Functor of C,D; :: thesis: for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let s be natural_transformation of F1,F2; :: thesis: for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let t be natural_transformation of G1,G2; :: thesis: for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let u be natural_transformation of H1,H2; :: thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 implies u (#) (t (#) s) = (u (#) t) (#) s )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 and
A3: H1 is_naturally_transformable_to H2 ; :: thesis: u (#) (t (#) s) = (u (#) t) (#) s
A4: ( u * (G2 * F2) = (u * G2) * F2 & H1 * (t * F2) = (H1 * t) * F2 ) by A2, A3, Th27, Th28;
A5: H1 * G1 is_naturally_transformable_to H1 * G2 by A2, Th20;
then A6: (H1 * G1) * F2 is_naturally_transformable_to (H1 * G2) * F2 by Th20;
A7: ( H1 * (G1 * s) = (H1 * G1) * s & (H1 * G1) * F1 is_naturally_transformable_to (H1 * G1) * F2 ) by A1, Th20, Th29;
A8: ( (H1 * G1) * F1 = H1 * (G1 * F1) & (H1 * G1) * F2 = H1 * (G1 * F2) ) by RELAT_1:36;
A9: H1 * G2 is_naturally_transformable_to H2 * G2 by A3, Th20;
then A10: (H1 * G2) * F2 is_naturally_transformable_to (H2 * G2) * F2 by Th20;
A11: ( (H1 * G2) * F2 = H1 * (G2 * F2) & (H2 * G2) * F2 = H2 * (G2 * F2) ) by RELAT_1:36;
( G1 * F2 is_naturally_transformable_to G2 * F2 & G1 * F1 is_naturally_transformable_to G1 * F2 ) by A1, A2, Th20;
hence u (#) (t (#) s) = (u * (G2 * F2)) `*` ((H1 * (t * F2)) `*` (H1 * (G1 * s))) by Th25
.= (((u * G2) * F2) `*` ((H1 * t) * F2)) `*` ((H1 * G1) * s) by A8, A11, A4, A7, A6, A10, NATTRA_1:26
.= (u (#) t) (#) s by A5, A9, Th26 ;
:: thesis: verum