let k, m, n, i be Nat; ( 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
; 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, Def9
.=
DigitDC (m,i,k)
by A5, A6, Th3
.=
DigA ((DecSD (m,(n + 1),k)),i)
by A4, Def9
;
hence
DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i)
; verum