for x being Element of (center R) st x <> 0. (center R) holds
x is left_invertible

proof

let x be Element of (center R); :: thesis: ( x <> 0. (center R) implies x is left_invertible )
assume A1: x <> 0. (center R) ; :: thesis: x is left_invertible
ex y being Element of (center R) st y * x = 1. (center R)

proof

reconsider a = x as Element of R by Lm1;
A2: 0. R = 0. (center R) by Def4;
then A3: a <> 0. R by A1;
then consider b being Element of R such that
A4: b * a = 1. R by ALGSTR_0:def 39, ALGSTR_0:def 27;
A5: a in center R ;
then A6: a * b = 1. R by A4, Lm3;
for s being Element of R holds b * s = s * b

proof

let s be Element of R; :: thesis: b * s = s * b
(1. R) * s = s * (1. R) ;
then (a * b) * s = (s * a) * b by A6, GROUP_1:def 3
.= (a * s) * b by A5, Lm3 ;
then ((a ") * (a * b)) * s = (a ") * ((a * s) * b) by GROUP_1:def 3
.= ((a ") * (a * s)) * b by GROUP_1:def 3
.= (((a ") * a) * s) * b by GROUP_1:def 3
.= ((1_ R) * s) * b by A3, VECTSP_2:9
.= s * b ;
hence s * b = ((a ") * (a * b)) * s
.= (((a ") * a) * b) * s by GROUP_1:def 3
.= ((1_ R) * b) * s by A3, VECTSP_2:9
.= b * s ;
:: thesis: verum

end;

then b in { x9 where x9 is Element of R : for s being Element of R holds x9 * s = s * x9 } ;
then b in the carrier of (center R) by Def4;
then reconsider y = b as Element of (center R) ;
take y ; :: thesis: y * x = 1. (center R)
thus y * x = b * a by Lm2
.= 1. R by A4
.= 1. (center R) by Def4 ; :: thesis: verum

end;

hence x is left_invertible by ALGSTR_0:def 27; :: thesis: verum

end;

hence center R is almost_left_invertible by ALGSTR_0:def 39; :: thesis: verum