theorem Th2: :: AIMLOOP:2

for Q being multLoop
for x, y, z, u being Element of Q st y * x = u & z * x = u holds
y = z