let i, k, n be Nat; :: thesis: ( i in Seg n & i > 1 & k >= 2 implies DigA ((DecSD (1,n,k)),i) = 0 )
assume that
A1: i in Seg n and
A2: i > 1 and
A3: k >= 2 ; :: thesis: DigA ((DecSD (1,n,k)),i) = 0
i - 1 > 1 - 1 by A2, XREAL_1:14;
then A4: i -' 1 > 0 by XREAL_0:def 2;
A5: Radix k > 2 by A3, RADIX_4:1;
then Radix k > 1 by XXREAL_0:2;
then A6: 1 div ((Radix k) |^ (i -' 1)) = 0 by A4, NAT_D:27, PEPIN:25;
DigA ((DecSD (1,n,k)),i) = DigitDC (1,i,k) by A1, RADIX_1:def 9
.= (1 mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) by RADIX_1:def 8
.= (1 div ((Radix k) |^ (i -' 1))) mod (Radix k) by A2, A5, RADIX_2:4 ;
hence DigA ((DecSD (1,n,k)),i) = 0 by A6, NAT_D:26; :: thesis: verum