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