:: deftheorem Def2 defines transformation FUNCTOR2:def 2 :
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for b₅ being ManySortedSet of the carrier of A holds
( b₅ is transformation of F1,F2 iff for a being Object of A holds b₅ . a is Morphism of (F1 . a),(F2 . a) );