let R be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: 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 )
let x, y be Element of (center R); :: thesis: for a, b being Element of R st x = a & y = b holds
( a + b = x + y & a * b = x * y )
let a, b be Element of R; :: thesis: ( x = a & y = b implies ( a + b = x + y & a * b = x * y ) )
assume A1: ( x = a & y = b ) ; :: thesis: ( a + b = x + y & a * b = x * y )
set ccR = the carrier of (center R);
A2: [x,y] in [: the carrier of (center R), the carrier of (center R):] by ZFMISC_1:87;
the addF of (center R) = the addF of R || the carrier of (center R) by Def4;
hence x + y = a + b by A1, A2, FUNCT_1:49; :: thesis: a * b = x * y
the multF of (center R) = the multF of R || the carrier of (center R) by Def4;
hence x * y = a * b by A1, A2, FUNCT_1:49; :: thesis: verum