theorem Th3: :: ISOCAT_1:5

for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2