for x being Element of (center R) holds x is right_complementable

proof

let x be Element of (center R); :: thesis: x is right_complementable
reconsider a = x as Element of R by Lm1;
consider b being Element of R such that
A1: a + b = 0. R by ALGSTR_0:def 11;
A2: for s being Element of R holds b * s = s * b

proof

let s be Element of R; :: thesis: b * s = s * b
x in the carrier of (center R) ;
then x in { x9 where x9 is Element of R : for s9 being Element of R holds x9 * s9 = s9 * x9 } by Def4;
then ex x9 being Element of R st
( x9 = x & ( for s9 being Element of R holds x9 * s9 = s9 * x9 ) ) ;
then A3: a * s = s * a ;
(0. R) * s = s * (0. R) ;
then (a * s) + (b * s) = s * (a + b) by A1, VECTSP_1:def 3;
then (a * s) + (b * s) = (s * a) + (s * b) by VECTSP_1:def 2;
then ((- (a * s)) + (a * s)) + (b * s) = (- (s * a)) + ((s * a) + (s * b)) by A3, RLVECT_1:def 3;
then (0. R) + (b * s) = (- (s * a)) + ((s * a) + (s * b)) by RLVECT_1:5;
then b * s = (- (s * a)) + ((s * a) + (s * b)) by RLVECT_1:4;
then b * s = ((- (s * a)) + (s * a)) + (s * b) by RLVECT_1:def 3;
then b * s = (0. R) + (s * b) by RLVECT_1:5;
hence b * s = s * b by RLVECT_1:4; :: 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) ;
x + y = a + b by Lm2
.= 0. (center R) by A1, Def4 ;
hence x is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;

hence center R is right_complementable by ALGSTR_0:def 16; :: thesis: verum