theorem Th9: :: AIMLOOP:9

for Q being multLoop
for x, y, z being Element of Q st a_op (x,y,z) = 1. Q holds
x * (y * z) = (x * y) * z