:: deftheorem Def27 defines `*` CAT_8:def 27 :
for C, D being category
for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
for T1 being natural_transformation of F1,F
for T2 being natural_transformation of F,F2
for b₈ being natural_transformation of F1,F2 holds
( b₈ = T2 `*` T1 iff for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
b₈ . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) );