let A, B, C, D be category; 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; 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; 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; 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; 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; 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; ( 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
; (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
; verum