:: deftheorem defines Radix RADIX_1:def 1 :
for n being Nat holds Radix n = 2 to_power n;