let R be non empty addLoopStr ; :: thesis: ( R is Abelian & R is left_add-cancelable implies R is right_add-cancelable )
assume ( R is Abelian & R is left_add-cancelable ) ; :: thesis: R is right_add-cancelable
then reconsider R = R as non empty left_add-cancelable Abelian addLoopStr ;
R is right_add-cancelable

proof

let a, b, c be Element of R; :: according to ALGSTR_0:def 4,ALGSTR_0:def 7 :: thesis: ( not b + a = c + a or b = c )
assume b + a = c + a ; :: thesis: b = c
hence b = c by ALGSTR_0:def 3; :: thesis: verum

end;

hence R is right_add-cancelable ; :: thesis: verum