let n, k be Nat; :: thesis: ( 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 ; :: thesis: SDDec (DecSD (0,n,k)) = 0
hence SDDec (DecSD (0,n,k)) = 0 by A1, RADIX_1:22; :: thesis: verum