theorem Th17: :: RADIX_3:17

for i, n, k being Nat
for a being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds
SD2SDSubDigit (a,i,k) is Element of k -SD_Sub