:: deftheorem Def5 defines `*` NATTRA_1:def 6 :
for A, B being Category
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) );