A2: Radix k > 2 by A1, RADIX_4:1;
then - (Radix k) < - 2 by XREAL_1:24;
then A3: (- (Radix k)) + 1 < (- 2) + 1 by XREAL_1:6;
A4: ( k -SD = { w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 ) } & 1 is Element of INT ) by INT_1:def 2, RADIX_1:def 2;
(Radix k) + (- 1) > 2 + (- 1) by A2, XREAL_1:6;
then 1 in k -SD by A3, A4;
hence ( ( i = m implies 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) ) by RADIX_1:14; :: thesis: verum