:: deftheorem defines mix-associative POLYALG1:def 1 :
for L being non empty doubleLoopStr
for A being non empty AlgebraStr over L holds
( A is mix-associative iff for a being Element of L
for x, y being Element of A holds a * (x * y) = (a * x) * y );