theorem :: AIMLOOP:4

for Q being multLoop
for x, y, z being Element of Q st y * x = z * x holds
y = z by Th2;