:: deftheorem Def7 defines natural_transformation FUNCTOR2:def 7 :
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for b₅ being transformation of F1,F2 holds
( b₅ is natural_transformation of F1,F2 iff for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b₅ ! b) * (F1 . f) = (F2 . f) * (b₅ ! a) );