:: deftheorem defines is_represented_by RADIX_1:def 12 :
for n, x, k being Nat holds
( x is_represented_by n,k iff x < (Radix k) |^ n );