:: deftheorem defines left_mult-cancelable ALGSTR_0:def 20 :
for M being multMagma
for x being Element of M holds
( x is left_mult-cancelable iff for y, z being Element of M st x * y = x * z holds
y = z );