:: deftheorem Def8 defines `*` FUNCTOR2:def 8 :
for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for b₈ being natural_transformation of F,F2 holds
( b₈ = t2 `*` t1 iff b₈ = t2 `*` t1 );