:: deftheorem Def4 defines center WEDDWITT:def 4 :
for R being non empty right_complementable right-distributive left-distributive well-unital add-associative right_zeroed associative doubleLoopStr
for b₂ being non empty strict commutative doubleLoopStr holds
( b₂ = center R iff ( the carrier of b₂ = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b₂ = the addF of R || the carrier of b₂ & the multF of b₂ = the multF of R || the carrier of b₂ & 0. b₂ = 0. R & 1. b₂ = 1. R ) );