let x, n, k, i be Nat; :: thesis: ( i in Seg n implies DigA ((DecSD (x,n,k)),i) >= 0 )
assume A1: i in Seg n ; :: thesis: 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 ; :: thesis: verum