set M = Trivial-addMagma ;
thus Trivial-addMagma is right_add-cancelable :: according to ALGSTR_0:def 8 :: thesis: Trivial-addMagma is left_add-cancelable

proof

let x, y, z be Element of Trivial-addMagma; :: according to ALGSTR_0:def 4,ALGSTR_0:def 7 :: thesis: ( y + x = z + x implies y = z )
assume y + x = z + x ; :: thesis: y = z
thus y = z by STRUCT_0:def 10; :: thesis: verum

end;

let x, y, z be Element of Trivial-addMagma; :: according to ALGSTR_0:def 3,ALGSTR_0:def 6 :: thesis: ( x + y = x + z implies y = z )
assume x + y = x + z ; :: thesis: y = z
thus y = z by STRUCT_0:def 10; :: thesis: verum