let n, k be Nat; ( n >= 1 implies SDDec (DecSD (0,n,k)) = 0 )
Radix k >= 0 + 1
by INT_1:7, RADIX_2:6;
then
(Radix k) |^ n >= 1
by PREPOWER:11;
then A1:
0 is_represented_by n,k
by RADIX_1:def 12;
assume
n >= 1
; SDDec (DecSD (0,n,k)) = 0
hence
SDDec (DecSD (0,n,k)) = 0
by A1, RADIX_1:22; verum