for x, y, z being Element of (center R) holds (x + y) + z = x + (y + z)

proof

let x, y, z be Element of (center R); :: thesis: (x + y) + z = x + (y + z)
reconsider a = x, b = y, c = z as Element of R by Lm1;
A1: y + z = b + c by Lm2;
x + y = a + b by Lm2;
hence (x + y) + z = (a + b) + c by Lm2
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A1, Lm2 ;
:: thesis: verum

end;

hence center R is add-associative by RLVECT_1:def 3; :: thesis: verum