:: deftheorem defines invertible NATTRA_1:def 10 :
for A, B being Category
for F1, F2 being Functor of A,B
for IT being transformation of F1,F2 holds
( IT is invertible iff for a being Object of A holds IT . a is invertible );