:: deftheorem defines DigitDC RADIX_1:def 8 :
for i, k, x being Nat holds DigitDC (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));