let R be Ring; :: thesis: ( R is almost_right_invertible & R is commutative implies R is almost_left_invertible )
assume AS: ( R is almost_right_invertible & R is commutative ) ; :: thesis: R is almost_left_invertible
now :: thesis: for x being Element of R st x <> 0. R holds
x is left_invertible
let x be Element of R; :: thesis: ( x <> 0. R implies x is left_invertible )
assume x <> 0. R ; :: thesis: x is left_invertible
then x is right_invertible by AS;
then consider y being Element of R such that
A1: x * y = 1. R ;
y * x = 1. R by A1, AS, GROUP_1:def 12;
hence x is left_invertible ; :: thesis: verum
end;
hence R is almost_left_invertible ; :: thesis: verum