thus
Z_3 is add-associative
:: thesis: ( Z_3 is right_zeroed & Z_3 is right_complementable )

reconsider x9 = x as Element of {0,1,2} ;

reconsider y = compl3 . x9 as Element of Z_3 ;

reconsider y9 = y as Element of {0,1,2} ;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. Z_3

A1: y9 = - x9 by Def17;

thus x + y = 0. Z_3 :: thesis: verum

proof

thus
Z_3 is right_zeroed
:: thesis: Z_3 is right_complementable
let x, y, z be Element of Z_3; :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)

reconsider X = x, Y = y, Z = z as Element of {0,1,2} ;

thus (x + y) + z = (X + Y) + Z by Lm6

.= X + (Y + Z) by Lm7

.= x + (y + z) by Lm6 ; :: thesis: verum

end;reconsider X = x, Y = y, Z = z as Element of {0,1,2} ;

thus (x + y) + z = (X + Y) + Z by Lm6

.= X + (Y + Z) by Lm7

.= x + (y + z) by Lm6 ; :: thesis: verum

proof

let x be Element of Z_3; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
let x be Element of Z_3; :: according to RLVECT_1:def 4 :: thesis: x + (0. Z_3) = x

reconsider X = x, a = 0 as Element of {0,1,2} by Def20;

thus x + (0. Z_3) = X + a by Def15

.= x by Lm7 ; :: thesis: verum

end;reconsider X = x, a = 0 as Element of {0,1,2} by Def20;

thus x + (0. Z_3) = X + a by Def15

.= x by Lm7 ; :: thesis: verum

reconsider x9 = x as Element of {0,1,2} ;

reconsider y = compl3 . x9 as Element of Z_3 ;

reconsider y9 = y as Element of {0,1,2} ;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. Z_3

A1: y9 = - x9 by Def17;

thus x + y = 0. Z_3 :: thesis: verum

proof
end;

per cases
( x = 0 or x = 1 or x = 2 )
by ENUMSET1:def 1;

end;

suppose A2:
x = 0
; :: thesis: x + y = 0. Z_3

then A3:
y9 = 0
by A1, Def12;

thus x + y = x9 + y9 by Def15

.= 0. Z_3 by A2, A3, Def13 ; :: thesis: verum

end;thus x + y = x9 + y9 by Def15

.= 0. Z_3 by A2, A3, Def13 ; :: thesis: verum