theorem Th19: :: FUNCTOR3:19

for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1)