theorem Th1: :: AIMLOOP:1

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