:: deftheorem defines is_naturally_transformable_to CAT_8:def 25 :
for C, D being category
for F1, F2 being Functor of C,D holds
( F1 is_naturally_transformable_to F2 iff ex T being Functor of C,D st T is_natural_transformation_of F1,F2 );