let R be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for x being Element of (center R) holds x is Element of R
let x be Element of (center R); :: thesis: x is Element of R
x in the carrier of (center R) ;
then x in { y where y is Element of R : for s being Element of R holds y * s = s * y } by Def4;
then ex y being Element of R st
( y = x & ( for s being Element of R holds y * s = s * y ) ) ;
hence x is Element of R ; :: thesis: verum