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