theorem Th11: :: FUNCTOR3:11

for A, B, C 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 p being transformation of F1,F2
for o being Object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)