let x, y, z be Scalar of Z_3; :: 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 that
A1: X = x and
A2: Y = y and
A3: 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) )
A4: ( x * y = X * Y & y * z = Y * Z ) by A1, A2, A3, Def16;
( x + y = X + Y & y + z = Y + Z ) by A1, A2, A3, Def15;
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, A3, A4, Def15, Def16; :: thesis: verum