:: deftheorem Def5 defines `*` FUNCTOR2:def 5 :
for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for b₈ being transformation of F,F2 holds
( b₈ = t2 `*` t1 iff for a being Object of A holds b₈ ! a = (t2 ! a) * (t1 ! a) );