let n, m, k, i be Nat; :: thesis: ( i in Seg n implies DigA (DecSD m,(n + 1),k),i = DigA (DecSD (m mod ((Radix k) |^ n)),n,k),i )
assume A1: i in Seg n ; :: thesis: DigA (DecSD m,(n + 1),k),i = DigA (DecSD (m mod ((Radix k) |^ n)),n,k),i
then A2: i <= n by FINSEQ_1:3;
then A3: i <= n + 1 by NAT_1:12;
1 <= i by A1, FINSEQ_1:3;
then A4: i in Seg (n + 1) by A3, FINSEQ_1:3;
(Radix k) |^ i divides (Radix k) |^ n by A2, RADIX_1:7;
then consider t being Nat such that
A5: (Radix k) |^ n = ((Radix k) |^ i) * t by NAT_D:def 3;
Radix k <> 0 by POWER:39;
then A6: t <> 0 by A5, PREPOWER:12;
DigA (DecSD (m mod ((Radix k) |^ n)),n,k),i = DigitDC (m mod ((Radix k) |^ n)),i,k by A1, RADIX_1:def 9
.= DigitDC m,i,k by A5, A6, RADIX_1:4
.= DigA (DecSD m,(n + 1),k),i by A4, RADIX_1:def 9 ;
hence DigA (DecSD m,(n + 1),k),i = DigA (DecSD (m mod ((Radix k) |^ n)),n,k),i ; :: thesis: verum