let n, m, k, i be Nat; :: thesis: ( i in Seg n implies DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i) )
assume A1: i in Seg n ; :: thesis: DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i)
then i <= n by FINSEQ_1:1;
then A2: i <= n + 1 by NAT_1:12;
1 <= i by A1, FINSEQ_1:1;
then A3: i in Seg (n + 1) by A2, FINSEQ_1:1;
DigA ((DecSD (m,n,k)),i) = DigitDC (m,i,k) by A1, RADIX_1:def 9
.= DigA ((DecSD (m,(n + 1),k)),i) by A3, RADIX_1:def 9 ;
hence DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i) ; :: thesis: verum