:: deftheorem defines SubDigit2 RADIX_2:def 1 :
for i, k, n being Nat
for x being Tuple of n, NAT holds SubDigit2 (x,i,k) = ((Radix k) |^ (i -' 1)) * (x . i);