:: deftheorem Def4 defines ! FUNCTOR2:def 4 :
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 t being transformation of F1,F2
for a being Object of A
for b₇ being Morphism of (F1 . a),(F2 . a) holds
( b₇ = t ! a iff b₇ = t . a );