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