let M be non empty commutative multLoopStr_0 ; :: thesis: ( M is almost_right_cancelable implies M is almost_left_cancelable )
assume A10: M is almost_right_cancelable ; :: thesis: M is almost_left_cancelable
let x be Element of M; :: according to ALGSTR_0:def 35 :: thesis: ( x = 0. M or x is left_mult-cancelable )
assume A11: x <> 0. M ; :: thesis: x is left_mult-cancelable
let y, z be Element of M; :: according to ALGSTR_0:def 20 :: thesis: ( not x * y = x * z or y = z )
assume x * y = x * z ; :: thesis: y = z
hence y = z by A10, A11, ALGSTR_0:def 21; :: thesis: verum