:: deftheorem Def1 defines * FUNCTOR3:def 1 :
for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for t being transformation of F1,F2
for G being covariant Functor of B,C st F1 is_transformable_to F2 holds
for b₈ being transformation of G * F1,G * F2 holds
( b₈ = G * t iff for o being Object of A holds b₈ . o = G . (t ! o) );