let M be non empty commutative multMagma ; :: thesis: ( M is right_mult-cancelable implies M is left_mult-cancelable )
assume A14: M is right_mult-cancelable ; :: thesis: M is left_mult-cancelable
let x, y, z be Element of M; :: according to ALGSTR_0:def 20,ALGSTR_0:def 23 :: thesis: ( not x * y = x * z or y = z )
assume x * y = x * z ; :: thesis: y = z
hence y = z by A14, ALGSTR_0:def 21; :: thesis: verum