theorem Th16: :: FUNCTOR3:16

for A, B, C, D being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
(H1 * q) * F1 = H1 * (q * F1)