len r = m + 2 by CARD_1:def 7;
then i in dom r by A1, 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 0 is Element of k -SD ) ) by RADIX_1:14; :: thesis: verum