let A, B, C, D be category; :: thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let F1, F2 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let G1, G2 be covariant Functor of B,C; :: thesis: for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let H1, H2 be covariant Functor of C,D; :: thesis: for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let t be transformation of F1,F2; :: thesis: for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let s be transformation of G1,G2; :: thesis: for u being transformation of H1,H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
let u be transformation of H1,H2; :: thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 implies (u (#) s) (#) t = u (#) (s (#) t) )
assume that
A1: F1 is_transformable_to F2 and
A2: G1 is_transformable_to G2 and
A3: H1 is_transformable_to H2 ; :: thesis: (u (#) s) (#) t = u (#) (s (#) t)
A4: ( G1 * F2 is_transformable_to G2 * F2 & G1 * F1 is_transformable_to G1 * F2 ) by A1, A2, Th10;
A5: ( (H1 * s) * F2 = H1 * (s * F2) & (H1 * G1) * t = H1 * (G1 * t) ) by A1, A2, Th16, Th17;
A6: ( (H1 * G2) * F2 = H1 * (G2 * F2) & (H2 * G2) * F2 = H2 * (G2 * F2) ) by FUNCTOR0:32;
A7: ( (H1 * G1) * F1 is_transformable_to (H1 * G1) * F2 & (u * G2) * F2 = u * (G2 * F2) ) by A1, A3, Th10, Th15;
A8: ( (H1 * G1) * F1 = H1 * (G1 * F1) & (H1 * G1) * F2 = H1 * (G1 * F2) ) by FUNCTOR0:32;
A9: H1 * G1 is_transformable_to H1 * G2 by A2, Th10;
then A10: (H1 * G1) * F2 is_transformable_to (H1 * G2) * F2 by Th10;
A11: H1 * G2 is_transformable_to H2 * G2 by A3, Th10;
then A12: (H1 * G2) * F2 is_transformable_to (H2 * G2) * F2 by Th10;
thus (u (#) s) (#) t = (((u * G2) * F2) `*` ((H1 * s) * F2)) `*` ((H1 * G1) * t) by A11, A9, Th14
.= (u * (G2 * F2)) `*` ((H1 * (s * F2)) `*` (H1 * (G1 * t))) by A12, A10, A7, A5, A8, A6, FUNCTOR2:6
.= u (#) (s (#) t) by A4, Th13 ; :: thesis: verum