:: deftheorem Def6 defines associative CAT_1:def 8 :
for C being non empty non void CatStr holds
( C is associative iff for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f );