let R be Ring; :: thesis: ( R is almost_left_cancelable & R is commutative implies R is almost_right_cancelable )
assume AS: ( R is almost_left_cancelable & R is commutative ) ; :: thesis: R is almost_right_cancelable

now :: thesis: for x being Element of R st x <> 0. R holds
x is right_mult-cancelable

let x be Element of R; :: thesis: ( x <> 0. R implies x is right_mult-cancelable )
assume x <> 0. R ; :: thesis: x is right_mult-cancelable
then AS1: x is left_mult-cancelable by AS;

now :: thesis: for y, z being Element of R st y * x = z * x holds
y = z

let y, z be Element of R; :: thesis: ( y * x = z * x implies y = z )
assume y * x = z * x ; :: thesis: y = z
then x * y = z * x by AS, GROUP_1:def 12
.= x * z by AS, GROUP_1:def 12 ;
hence y = z by AS1; :: thesis: verum

end;

hence x is right_mult-cancelable ; :: thesis: verum

end;

hence R is almost_right_cancelable ; :: thesis: verum