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

proof

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

end;

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