:: deftheorem Def2 defines \ AIMLOOP:def 2 :
for Q being non empty left_mult-cancelable invertible multLoopStr
for x, y, b₄ being Element of Q holds
( b₄ = x \ y iff x * b₄ = y );