:: deftheorem defines is_natural_transformation_of CAT_8:def 24 :
for C1, C2 being category
for F1, F2, T being Functor of C1,C2 holds
( T is_natural_transformation_of F1,F2 iff for f1, f2 being morphism of C1 st f1 |> f2 holds
( T . f1 |> F1 . f2 & F2 . f1 |> T . f2 & T . (f1 (*) f2) = (T . f1) (*) (F1 . f2) & T . (f1 (*) f2) = (F2 . f1) (*) (T . f2) ) );