:: deftheorem defines a_op AIMLOOP:def 14 :
for Q being multLoop
for x, y, z being Element of Q holds a_op (x,y,z) = (x * (y * z)) \ ((x * y) * z);