theorem Th36: :: ISOCAT_2:38

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_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
<:F1,F2:> is_naturally_transformable_to <:G1,G2:>