:: deftheorem defines SDSub2INTDigit RADIX_3:def 10 :
for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds SDSub2INTDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));