theorem Th24: :: MOD_2:24

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