:: deftheorem Def7 defines natural_transformation NATTRA_1:def 8 :
for A, B being Category
for F1, F2 being 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 Hom (a,b) <> {} holds
for f being Morphism of a,b holds (b₅ . b) * (F1 /. f) = (F2 /. f) * (b₅ . a) );