:: deftheorem defines K_op AIMLOOP:def 13 :
for Q being multLoop
for x, y being Element of Q holds K_op (x,y) = (y * x) \ (x * y);