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