len r = m + 2 by CARD_1:def 7;
then i in dom r by A2, FINSEQ_1:def 3;
then r . i in rng r by FUNCT_1:def 3;
hence ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (Radix k) - 1 is Element of k -SD ) ) by A1, RADIX_5:1; :: thesis: verum