theorem Th23: :: MOD_2:23

for x, y being Scalar of Z_3
for X, Y being Element of {0,1,2} st X = x & Y = y holds
( x + y = X + Y & x * y = X * Y & - x = - X )