:: deftheorem Def3 defines (*) CAT_6:def 3 :
for C being CategoryStr
for f1, f2 being morphism of C st f1 |> f2 holds
f1 (*) f2 = the composition of C . (f1,f2);