let n, k be Nat; :: thesis: ( n >= 1 & k >= 2 implies SDDec (DecSD (1,n,k)) = 1 )
assume that
A1: n >= 1 and
A2: k >= 2 ; :: thesis: SDDec (DecSD (1,n,k)) = 1
A3: Radix k > 2 by A2, RADIX_4:1;
Radix k >= 0 + 1 by INT_1:7, RADIX_2:6;
then (Radix k) |^ n >= Radix k by A1, PREPOWER:12;
then (Radix k) |^ n >= 2 by A3, 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:22; :: thesis: verum