:: deftheorem defines R_map AIMLOOP:def 6 :
for Q being non empty right_mult-cancelable invertible multLoopStr
for u, x, y being Element of Q holds R_map (u,x,y) = ((u * x) * y) / (x * y);