let k be Nat; :: thesis: Radix k > 0
Radix k = 2 to_power k by RADIX_1:def 1;
hence Radix k > 0 by POWER:34; :: thesis: verum