:: deftheorem Def5 defines natural_equivalence FUNCTOR3:def 5 :
for A, B being category
for F1, F2 being covariant Functor of A,B st F1,F2 are_naturally_equivalent holds
for b₅ being natural_transformation of F1,F2 holds
( b₅ is natural_equivalence of F1,F2 iff for a being Object of A holds b₅ ! a is iso );