let R be Ring; :: thesis: ( R is almost_right_cancelable & R is commutative implies R is almost_left_cancelable )
assume AS: ( R is almost_right_cancelable & R is commutative ) ; :: thesis: R is almost_left_cancelable
now :: thesis: for x being Element of R st x <> 0. R holds
x is left_mult-cancelable
let x be Element of R; :: thesis: ( x <> 0. R implies x is left_mult-cancelable )
assume x <> 0. R ; :: thesis: x is left_mult-cancelable
then AS1: x is right_mult-cancelable by AS;
now :: thesis: for y, z being Element of R st x * y = x * z holds
y = z
let y, z be Element of R; :: thesis: ( x * y = x * z implies y = z )
assume x * y = x * z ; :: thesis: y = z
then y * x = x * z by AS, GROUP_1:def 12
.= z * x by AS, GROUP_1:def 12 ;
hence y = z by AS1; :: thesis: verum
end;
hence x is left_mult-cancelable ; :: thesis: verum
end;
hence R is almost_left_cancelable ; :: thesis: verum