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

( 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