theorem Th17: :: FUNCTOR3:17

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