:: deftheorem Def11 defines " NATTRA_1:def 12 :
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1 being transformation of F1,F2 st t1 is invertible holds
for b₆ being transformation of F2,F1 holds
( b₆ = t1 " iff for a being Object of A holds b₆ . a = (t1 . a) " );