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:1;

then A3: i <= n + 1 by NAT_1:12;

1 <= i by A1, FINSEQ_1:1;

then A4: i in Seg (n + 1) by A3, FINSEQ_1:1;

(Radix k) |^ i divides (Radix k) |^ n by A2, NEWTON:89;

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:34;

then A6: t <> 0 by A5, PREPOWER:5;

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:3

.= 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

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:1;

then A3: i <= n + 1 by NAT_1:12;

1 <= i by A1, FINSEQ_1:1;

then A4: i in Seg (n + 1) by A3, FINSEQ_1:1;

(Radix k) |^ i divides (Radix k) |^ n by A2, NEWTON:89;

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:34;

then A6: t <> 0 by A5, PREPOWER:5;

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:3

.= 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