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