:: deftheorem Def4 defines . NATTRA_1:def 5 :
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being Object of A holds t . a = t . a;