:: deftheorem Def3 defines id NATTRA_1:def 4 :
for A, B being Category
for F being Functor of A,B
for b₄ being transformation of F,F holds
( b₄ = id F iff for a being Object of A holds b₄ . a = id (F . a) );