:: deftheorem defines DigB RADIX_1:def 4 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds DigB (x,i) = DigA (x,i);