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 A1: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1 is_transformable_to H2 ) ; :: thesis: (u (#) s) (#) t = u (#) (s (#) t)
then A2: ( H1 * G2 is_transformable_to H2 * G2 & H1 * G1 is_transformable_to H1 * G2 ) by Th10;
then A3: ( (H1 * G2) * F2 is_transformable_to (H2 * G2) * F2 & (H1 * G1) * F2 is_transformable_to (H1 * G2) * F2 & (H1 * G1) * F1 is_transformable_to (H1 * G1) * F2 ) by A1, Th10;
A4: ( G1 * F2 is_transformable_to G2 * F2 & G1 * F1 is_transformable_to G1 * F2 ) by A1, Th10;
A5: ( (u * G2) * F2 = u * (G2 * F2) & (H1 * s) * F2 = H1 * (s * F2) & (H1 * G1) * t = H1 * (G1 * t) ) by A1, Th15, Th16, Th17;
A6: ( (H1 * G1) * F1 = H1 * (G1 * F1) & (H1 * G1) * F2 = H1 * (G1 * F2) & (H1 * G2) * F2 = H1 * (G2 * F2) & (H2 * G2) * F2 = H2 * (G2 * F2) ) by FUNCTOR0:33;
thus (u (#) s) (#) t = (((u * G2) * F2) `*` ((H1 * s) * F2)) `*` ((H1 * G1) * t) by A2, Th14
.= (u * (G2 * F2)) `*` ((H1 * (s * F2)) `*` (H1 * (G1 * t))) by A3, A5, A6, FUNCTOR2:8
.= u (#) (s (#) t) by A4, Th13 ; :: thesis: verum