theorem Th15: :: FUNCTOR3:15

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