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 GROUP_1:def 3
.= x * (y * z) by A1, Lm2 ;
:: thesis: verum

end;

hence center R is associative ; :: thesis: verum