:: deftheorem Def2 defines * FUNCTOR3:def 2 :
for A, B, C being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for F being covariant Functor of A,B
for s being transformation of G1,G2 st G1 is_transformable_to G2 holds
for b₈ being transformation of G1 * F,G2 * F holds
( b₈ = s * F iff for o being Object of A holds b₈ . o = s ! (F . o) );