theorem Th5: :: RADIX_6:5
for x, n, k, i being Nat st i in Seg n holds
DigA ((DecSD (x,n,k)),i) >= 0