for k being Nat holds Radix k > 0