:: deftheorem Def10 defines associative CAT_6:def 10 :
for C being CategoryStr holds
( C is associative iff for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds
f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 );