:: deftheorem defines / ALGSTR_0:def 30 :
for M being multLoopStr
for x being Element of M st x is left_invertible & x is right_mult-cancelable holds
for b₃ being Element of M holds
( b₃ = / x iff b₃ * x = 1. M );