:: deftheorem Def7 defines SD2SDSubDigitS RADIX_3:def 7 :
for i, k, n being Nat
for x being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds
SD2SDSubDigitS (x,i,k) = SD2SDSubDigit (x,i,k);