for x being Element of (center R) holds
( x * (1. (center R)) = x & (1. (center R)) * x = x )

proof

let x be Element of (center R); :: thesis: ( x * (1. (center R)) = x & (1. (center R)) * x = x )
reconsider a = x as Element of R by Lm1;
A1: 1. R = 1. (center R) by Def4;
hence x * (1. (center R)) = a * (1. R) by Lm2
.= a
.= x ;
:: thesis: (1. (center R)) * x = x
thus (1. (center R)) * x = (1. R) * a by A1, Lm2
.= a
.= x ; :: thesis: verum

end;

hence center R is well-unital ; :: thesis: verum