for v being Element of (center R) holds v + (0. (center R)) = v

proof

let v be Element of (center R); :: thesis: v + (0. (center R)) = v
reconsider a = v as Element of R by Lm1;
0. (center R) = 0. R by Def4;
hence v + (0. (center R)) = a + (0. R) by Lm2
.= a by RLVECT_1:def 4
.= v ;
:: thesis: verum

end;

hence center R is right_zeroed by RLVECT_1:def 4; :: thesis: verum