let n, m, k, i be Nat; :: thesis: ( i in Seg n & 2 <= k implies DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) )
assume A1: i in Seg n ; :: thesis: ( not 2 <= k or DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) )
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A2: 1 <= i by A1, FINSEQ_1:1;
i <= n by A1, FINSEQ_1:1;
then A3: i <= n + 1 by NAT_1:12;
then A4: i in Seg (n + 1) by A2, FINSEQ_1:1;
i <= (n + 1) + 1 by A3, NAT_1:12;
then A5: i in Seg ((n + 1) + 1) by A2, FINSEQ_1:1;
set M = m mod ((Radix k) |^ n);
assume A6: 2 <= k ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)
A7: DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) = SD2SDSubDigitS ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i,k) by A4, Def8
.= SD2SDSubDigit ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i,k) by A6, A4, Def7
.= (SDSub_Add_Data ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),(i -' 1))),k)) by A1, Def6
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),(i -' 1))),k)) by A1, Lm5 ;

now :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)

per cases ( i = 1 or i <> 1 ) ;

suppose A8: i = 1 ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)

then A9: DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) = (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),0)),k)) by A7, XREAL_1:232
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def 3
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + 0 by Th16 ;
DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = SD2SDSubDigitS ((DecSD (m,(n + 1),k)),i,k) by A5, Def8
.= SD2SDSubDigit ((DecSD (m,(n + 1),k)),i,k) by A6, A5, Def7
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,(n + 1),k)),(i -' 1))),k)) by A4, Def6
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,(n + 1),k)),0)),k)) by A8, XREAL_1:232
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def 3
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + 0 by Th16 ;
hence DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) by A9; :: thesis: verum

end;

suppose A10: i <> 1 ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)

i <= n by A1, FINSEQ_1:1;
then A11: i -' 1 <= n by NAT_D:44;
1 < i by A2, A10, XXREAL_0:1;
then 0 + 1 <= i -' 1 by INT_1:7, JORDAN12:1;
then i -' 1 in Seg n by A11, FINSEQ_1:1;
then DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) = (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,(n + 1),k)),(i -' 1))),k)) by A7, Lm5
.= SD2SDSubDigit ((DecSD (m,(n + 1),k)),i,k) by A4, Def6
.= SD2SDSubDigitS ((DecSD (m,(n + 1),k)),i,k) by A6, A5, Def7
.= DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) by A5, Def8 ;
hence DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) ; :: thesis: verum

end;

end;

end;

hence DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) ; :: thesis: verum