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

( (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