theorem Th58: :: CAT_8:58

for C1, C2 being category
for F1, F2, T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )