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