let M be non empty Abelian addMagma ; :: thesis: ( M is right_add-cancelable implies M is left_add-cancelable )
assume A1: M is right_add-cancelable ; :: thesis: M is left_add-cancelable
let x, y, z be Element of M; :: according to ALGSTR_0:def 3,ALGSTR_0:def 6 :: thesis: ( not x + y = x + z or y = z )
assume x + y = x + z ; :: thesis: y = z
hence y = z by A1, ALGSTR_0:def 4; :: thesis: verum