:: deftheorem defines DigB_SDSub RADIX_3:def 9 :
for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds DigB_SDSub (x,i) = DigA_SDSub (x,i);