:: deftheorem Def12 defines " NATTRA_1:def 13 :
for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
t1 " = t1 " ;