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