len r = m + 2 by FINSEQ_1:def 18;
then i in dom r by A1, FINSEQ_1:def 3;
then r . i in rng r by FUNCT_1:def 5;
hence ( ( i < m implies r . i is Element of k -SD ) & ( not i < m implies 0 is Element of k -SD ) ) by RADIX_1:16; :: thesis: verum