:: deftheorem Def8 defines associative ALTCAT_2:def 8 :
for C being non empty transitive AltCatStr holds
( C is associative iff for o1, o2, o3, o4 being Object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) );