let n, k, x be Nat; :: thesis: ( n >= 1 & x needs_digits_of n,k implies DigA (DecSD x,n,k),n > 0 )
assume that
A1: n >= 1 and
A2: x needs_digits_of n,k ; :: thesis: DigA (DecSD x,n,k),n > 0
x < (Radix k) |^ n by A2, Def7;
then A3: x mod ((Radix k) |^ n) = x by NAT_D:24;
n in Seg n by A1, FINSEQ_1:5;
then A4: DigA (DecSD x,n,k),n = DigitDC x,n,k by RADIX_1:def 9
.= x div ((Radix k) |^ (n -' 1)) by A3, RADIX_1:def 8 ;
A5: (Radix k) |^ (n -' 1) > 0 by PREPOWER:13, RADIX_2:6;
x >= (Radix k) |^ (n -' 1) by A2, Def7;
hence DigA (DecSD x,n,k),n > 0 by A4, A5, NAT_2:15; :: thesis: verum