let n, k, x be Nat; ( 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
; 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; verum