let n, k, m, 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 )
assume A2: 2 <= k ; :: thesis: 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 13;
set M = m mod ((Radix k) |^ n);
A3: ( 1 <= i & i <= n ) by A1, FINSEQ_1:3;
then A4: i <= n + 1 by NAT_1:12;
then A5: i in Seg (n + 1) by A3, FINSEQ_1:3;
i <= (n + 1) + 1 by A4, NAT_1:12;
then A6: i in Seg ((n + 1) + 1) by A3, FINSEQ_1:3;
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 A5, Def8
.= SD2SDSubDigit (DecSD (m mod ((Radix k) |^ n)),n,k),i,k by A2, A5, 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

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:234
.= (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 A2, Th17 ;
DigA_SDSub (SD2SDSub (DecSD m,(n + 1),k)),i = SD2SDSubDigitS (DecSD m,(n + 1),k),i,k by A6, Def8
.= SD2SDSubDigit (DecSD m,(n + 1),k),i,k by A2, A6, 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 A5, 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:234
.= (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 A2, Th17 ;
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 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 1 < i by A3, XXREAL_0:1;
then A10: 0 + 1 <= i -' 1 by INT_1:20, JORDAN12:1;
i <= n by A1, FINSEQ_1:3;
then i -' 1 <= n by NAT_D:44;
then i -' 1 in Seg n by A10, FINSEQ_1:3;
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 A5, Def6
.= SD2SDSubDigitS (DecSD m,(n + 1),k),i,k by A2, A6, Def7
.= DigA_SDSub (SD2SDSub (DecSD m,(n + 1),k)),i by A6, 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