let x, y, z be Scalar of Z3 ; :: thesis: 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) )
let X, Y, Z be Element of {0 ,1,2}; :: thesis: ( X = x & Y = y & Z = z implies ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) ) )
assume A1: ( X = x & Y = y & Z = z ) ; :: thesis: ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
then ( x + y = X + Y & y + z = Y + Z & x * y = X * Y & y * z = Y * Z ) by Th33;
hence ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) ) by A1, Th33; :: thesis: verum