:: deftheorem Def4 defines center WEDDWITT:def 4 :
for R being Skew-Field
for b₂ being strict Field 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 ) );