A2: k -SD = { w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 ) } by RADIX_1:def 2;
A3: (- (Radix k)) + 1 in k -SD

proof

Radix k > 2 by A1, RADIX_4:1;
then Radix k > 1 by XXREAL_0:2;
then (Radix k) + (Radix k) > 1 + 1 by XREAL_1:10;
then A4: (Radix k) - 1 > 1 - (Radix k) by XREAL_1:23;
(- (Radix k)) + 1 is Element of INT by INT_1:def 2;
hence (- (Radix k)) + 1 in k -SD by A2, A4; :: thesis: verum

end;

1 in k -SD

proof

A5: Radix k > 2 by A1, RADIX_4:1;
then A6: (Radix k) + (- 1) > 2 + (- 1) by XREAL_1:8;
- (Radix k) < - 2 by A5, XREAL_1:26;
then A7: (- (Radix k)) + 1 < (- 2) + 1 by XREAL_1:8;
1 is Element of INT by INT_1:def 2;
hence 1 in k -SD by A2, A6, A7; :: thesis: verum

end;

hence ( ( i > m implies 0 is Element of k -SD ) & ( i = m implies 1 is Element of k -SD ) & ( not i > m & not i = m implies (- (Radix k)) + 1 is Element of k -SD ) ) by A3, RADIX_1:16; :: thesis: verum