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 ;

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)end;

hence
DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)
; :: thesis: verumper cases
( i = 1 or i <> 1 )
;

end;

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;.= (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

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;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