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

proof

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

end;

hence center R is distributive ; :: thesis: verum