:: deftheorem Def2 defines transformation NATTRA_1:def 3 :
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for b₅ being Function of the carrier of A, the carrier' of B holds
( b₅ is transformation of F1,F2 iff for a being Object of A holds b₅ . a is Morphism of F1 . a,F2 . a );