theorem :: WEDDWITT:42

for R being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for x, y being Element of (center R)
for a, b being Element of R st x = a & y = b holds
( a + b = x + y & a * b = x * y ) by Lm2;