theorem Th31: :: ISOCAT_2:33

for A, B, C being Category
for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t