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;
then A3: x mod ((Radix k) |^ n) = x by NAT_D:24;
n in Seg n by A1, FINSEQ_1:3;
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:6, RADIX_2:6;
x >= (Radix k) |^ (n -' 1) by A2;
hence DigA ((DecSD (x,n,k)),n) > 0 by A4, A5, NAT_2:13; :: thesis: verum