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

proof

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;

thus Z_3 is right_zeroed :: thesis: Z_3 is right_complementable

proof

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;

let x be Element of Z_3; :: according to ALGSTR_0:def 16 :: thesis: x 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

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

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;

suppose A4: x = 1 ; :: thesis: x + y = 0. Z_3

then A5: y9 = 2 by A1, Def12;
thus x + y = x9 + y9 by Def15
.= 0. Z_3 by A4, A5, Def13 ; :: thesis: verum

end;

suppose A6: x = 2 ; :: thesis: x + y = 0. Z_3

then A7: y9 = 1 by A1, Def12;
thus x + y = x9 + y9 by Def15
.= 0. Z_3 by A6, A7, Def13 ; :: thesis: verum

end;

end;

end;