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 (() |^ 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 (() |^ n)),n,k))),i) )
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A2: 1 <= i by ;
i <= n by ;
then A3: i <= n + 1 by NAT_1:12;
then A4: i in Seg (n + 1) by ;
i <= (n + 1) + 1 by ;
then A5: i in Seg ((n + 1) + 1) by ;
set M = m mod (() |^ n);
assume A6: 2 <= k ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod (() |^ n)),n,k))),i)
A7: DigA_SDSub ((SD2SDSub (DecSD ((m mod (() |^ n)),n,k))),i) = SD2SDSubDigitS ((DecSD ((m mod (() |^ n)),n,k)),i,k) by
.= SD2SDSubDigit ((DecSD ((m mod (() |^ n)),n,k)),i,k) by A6, A4, Def7
.= (SDSub_Add_Data ((DigA ((DecSD ((m mod (() |^ n)),n,k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod (() |^ n)),n,k)),(i -' 1))),k)) by
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod (() |^ n)),n,k)),(i -' 1))),k)) by ;
now :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod (() |^ 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 (() |^ n)),n,k))),i)
then A9: DigA_SDSub ((SD2SDSub (DecSD ((m mod (() |^ n)),n,k))),i) = (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod (() |^ n)),n,k)),0)),k)) by
.= (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
.= 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
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,(n + 1),k)),0)),k)) by
.= (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 (() |^ 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 (() |^ n)),n,k))),i)
i <= n by ;
then A11: i -' 1 <= n by NAT_D:44;
1 < i by ;
then 0 + 1 <= i -' 1 by ;
then i -' 1 in Seg n by ;
then DigA_SDSub ((SD2SDSub (DecSD ((m mod (() |^ 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
.= SD2SDSubDigit ((DecSD (m,(n + 1),k)),i,k) by
.= SD2SDSubDigitS ((DecSD (m,(n + 1),k)),i,k) by A6, A5, Def7
.= DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) by ;
hence DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod (() |^ 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 (() |^ n)),n,k))),i) ; :: thesis: verum