:: deftheorem Def26 defines natural_transformation CAT_8:def 26 :
for C, D being category
for F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F2 holds
for b₅ being Functor of C,D holds
( b₅ is natural_transformation of F1,F2 iff b₅ is_natural_transformation_of F1,F2 );