r . i is Element of k -SD

proof

len r = m + 2 by FINSEQ_1:def 18;
then i in dom r by A2, FINSEQ_1:def 3;
then ( r . i in rng r & rng r c= k -SD ) by FUNCT_1:def 5;
hence r . i is Element of k -SD ; :: thesis: verum

end;

hence ( ( i >= m implies r . i is Element of k -SD ) & ( i < m implies (Radix k) - 1 is Element of k -SD ) ) by A1, RADIX_5:1; :: thesis: verum