let x, y be Scalar of Z3 ; :: thesis: 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 )
let X, Y be Element of {0 ,1,2}; :: thesis: ( X = x & Y = y implies ( x + y = X + Y & x * y = X * Y & - x = - X ) )
assume that
A1: X = x and
A2: Y = y ; :: thesis: ( x + y = X + Y & x * y = X * Y & - x = - X )
thus x + y = X + Y by A1, A2, Def18; :: thesis: ( x * y = X * Y & - x = - X )
thus x * y = X * Y by A1, A2, Def19; :: thesis: - x = - X
reconsider a = - X as Element of Z3 ;
x + a = X + (- X) by A1, Def18
.= 0. Z3 by Lm7 ;
hence - x = - X by RLVECT_1:def 11; :: thesis: verum