:: deftheorem defines L_map AIMLOOP:def 5 :
for Q being non empty left_mult-cancelable invertible multLoopStr
for u, x, y being Element of Q holds L_map (u,x,y) = (y * x) \ (y * (x * u));