theorem Th12: :: FUNCTOR3:12

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