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