let x, n, k, i be Nat; ( i in Seg n implies DigA ((DecSD (x,n,k)),i) >= 0 )
assume A1:
i in Seg n
; DigA ((DecSD (x,n,k)),i) >= 0
then A2:
i >= 1
by FINSEQ_1:1;
DigA ((DecSD (x,n,k)),i) =
DigitDC (x,i,k)
by A1, RADIX_1:def 9
.=
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1))
by RADIX_1:def 8
.=
(x div ((Radix k) |^ (i -' 1))) mod (Radix k)
by A2, RADIX_2:4, RADIX_2:6
;
hence
DigA ((DecSD (x,n,k)),i) >= 0
; verum