let x, y be Scalar of Z_3; :: 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, Def15; :: thesis: ( x * y = X * Y & - x = - X )
thus x * y = X * Y by A1, A2, Def16; :: thesis: - x = - X
reconsider a = - X as Element of Z_3 ;
x + a = X + (- X) by A1, Def15
.= 0. Z_3 by Lm7 ;
hence - x = - X by RLVECT_1:def 10; :: thesis: verum