theorem Th18: :: FUNCTOR3:18

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 (idt G1) * F1 = idt (G1 * F1)