theorem Th34: :: ISOCAT_2:36

for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
<:F1,F2:> is_transformable_to <:G1,G2:> by Lm3;