:: deftheorem Def6 defines " FUNCTOR3:def 6 :
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
for b₆ being natural_equivalence of F2,F1 holds
( b₆ = e " iff for a being Object of A holds b₆ . a = (e ! a) " );