theorem :: FUNCTOR3:27

for A, B, C, D being 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)