theorem Th10: :: FUNCTOR3:10
for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2