len r = m + 2 by CARD_1:def 7;
then i in dom r by A2, FINSEQ_1:def 3;
then A3: r . i in rng r by FUNCT_1:def 3;
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:8;
then A4: (Radix k) - 1 > 1 - (Radix k) by XREAL_1:21;
A5: (- (Radix k)) + 1 is Element of INT by INT_1:def 2;
k -SD = { w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 ) } by RADIX_1:def 2;
then (- (Radix k)) + 1 in k -SD by A4, A5;
hence ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (- (Radix k)) + 1 is Element of k -SD ) ) by A3; :: thesis: verum