defpred S_{1}[ Nat] means for k, x being Nat st k >= 2 & x is_represented_by $1,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,$1,k)));

let n be Nat; :: thesis: ( n >= 1 implies for k, x being Nat st k >= 2 & x is_represented_by n,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k))) )

assume A1: n >= 1 ; :: thesis: for k, x being Nat st k >= 2 & x is_represented_by n,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))

A2: for n being Nat st n >= 1 & S_{1}[n] holds

S_{1}[n + 1]
_{1}[1]

S_{1}[n]
from NAT_1:sch 8(A50, A2);

hence for k, x being Nat st k >= 2 & x is_represented_by n,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k))) by A1; :: thesis: verum

x = SDSub2IntOut (SD2SDSub (DecSD (x,$1,k)));

let n be Nat; :: thesis: ( n >= 1 implies for k, x being Nat st k >= 2 & x is_represented_by n,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k))) )

assume A1: n >= 1 ; :: thesis: for k, x being Nat st k >= 2 & x is_represented_by n,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))

A2: for n being Nat st n >= 1 & S

S

proof

A50:
S
let n be Nat; :: thesis: ( n >= 1 & S_{1}[n] implies S_{1}[n + 1] )

assume that

A3: n >= 1 and

A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

A5: n in Seg n by A3, FINSEQ_1:3;

let k, x be Nat; :: thesis: ( k >= 2 & x is_represented_by n + 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) )

assume that

A6: k >= 2 and

A7: x is_represented_by n + 1,k ; :: thesis: x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k)))

reconsider k = k as Element of NAT by ORDINAL1:def 12;

set xn = x mod ((Radix k) |^ n);

set RN1 = (Radix k) |^ (n + 1);

set RN = (Radix k) |^ n;

A8: (n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:3;

A9: SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k) = ((Radix k) |^ (n + 1)) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) by NAT_D:34

.= ((Radix k) |^ (n + 1)) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by A8, Def8

.= ((Radix k) |^ (n + 1)) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by A6, A8, Def7

.= ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(((n + 1) + 1) -' 1))),k)) by Def6

.= ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) by NAT_D:34 ;

set XN = SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k));

set X = SD2SDSub (DecSD (x,(n + 1),k));

deffunc H_{1}( Nat) -> Element of INT = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),$1,k);

consider xp being FinSequence of INT such that

A10: len xp = n + 1 and

A11: for i being Nat st i in dom xp holds

xp . i = H_{1}(i)
from FINSEQ_2:sch 1();

A12: dom xp = Seg (n + 1) by A10, FINSEQ_1:def 3;

A13: len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (n + 1) + 1 by CARD_1:def 7;

A14: for j being Nat st 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) holds

(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j

then x mod ((Radix k) |^ n) < (Radix k) |^ n by NAT_D:1, PREPOWER:6;

then x mod ((Radix k) |^ n) is_represented_by n,k ;

then A22: x mod ((Radix k) |^ n) = SDSub2IntOut (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) by A4, A6

.= Sum (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) ;

A23: n + 1 in Seg (n + 1) by FINSEQ_1:3;

then A24: n + 1 in Seg ((n + 1) + 1) by FINSEQ_2:8;

consider xpp being FinSequence of INT such that

A25: len xpp = n and

A26: for i being Nat st i in dom xpp holds

xpp . i = H_{1}(i)
from FINSEQ_2:sch 1();

A27: dom xpp = Seg n by A25, FINSEQ_1:def 3;

A28: for j being Nat st 1 <= j & j <= len xp holds

xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j_{2}( Nat) -> Element of INT = SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),$1,k);

consider xnpp being FinSequence of INT such that

A32: len xnpp = n and

A33: for i being Nat st i in dom xnpp holds

xnpp . i = H_{2}(i)
from FINSEQ_2:sch 1();

A34: dom xnpp = Seg n by A32, FINSEQ_1:def 3;

for j being Nat st 1 <= j & j <= len xnpp holds

xnpp . j = xpp . j

A37: len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) = n + 1 by CARD_1:def 7;

A38: for j being Nat st 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) holds

(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j

then A45: xp = xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*> by A28, FINSEQ_1:14;

len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) = (n + 1) + 1 by A10, FINSEQ_2:16;

then len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) by CARD_1:def 7;

then SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))) = xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*> by A14, FINSEQ_1:14;

then A46: Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (Sum xp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k)) by RVSUM_1:74

.= ((Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k)) by A45, A36, RVSUM_1:74 ;

set RNDIG = ((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)));

set RNSDC = ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k));

A47: Radix k > 0 by RADIX_2:6;

len (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) = n + 1 by A32, FINSEQ_2:16;

then SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) = xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*> by A37, A38, FINSEQ_1:14;

then A48: (x mod ((Radix k) |^ n)) + 0 = (Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k)) by A22, RVSUM_1:74;

A49: SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k) = ((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) by NAT_D:34

.= ((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),(n + 1),k)) by A24, Def8

.= ((Radix k) |^ n) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),(n + 1),k)) by A6, A24, Def7

.= ((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))),k))) by A23, Def6

.= ((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NAT_D:34

.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))

.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NEWTON:6 ;

SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k) = ((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1))) by NAT_D:34

.= ((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k)) by A23, Def8

.= ((Radix k) |^ n) * (SD2SDSubDigit ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k)) by A23, A6, Def7

.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1))),k)) by Def6

.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)),k)) by NAT_D:34

.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)) by A5, Lm5 ;

then Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (((x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) - (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by A46, A48, A49, A9

.= (x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (x div ((Radix k) |^ n))) by A7, RADIX_1:24 ;

hence x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) by A47, NAT_D:2, PREPOWER:6; :: thesis: verum

end;assume that

A3: n >= 1 and

A4: S

A5: n in Seg n by A3, FINSEQ_1:3;

let k, x be Nat; :: thesis: ( k >= 2 & x is_represented_by n + 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) )

assume that

A6: k >= 2 and

A7: x is_represented_by n + 1,k ; :: thesis: x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k)))

reconsider k = k as Element of NAT by ORDINAL1:def 12;

set xn = x mod ((Radix k) |^ n);

set RN1 = (Radix k) |^ (n + 1);

set RN = (Radix k) |^ n;

A8: (n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:3;

A9: SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k) = ((Radix k) |^ (n + 1)) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) by NAT_D:34

.= ((Radix k) |^ (n + 1)) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by A8, Def8

.= ((Radix k) |^ (n + 1)) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by A6, A8, Def7

.= ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(((n + 1) + 1) -' 1))),k)) by Def6

.= ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) by NAT_D:34 ;

set XN = SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k));

set X = SD2SDSub (DecSD (x,(n + 1),k));

deffunc H

consider xp being FinSequence of INT such that

A10: len xp = n + 1 and

A11: for i being Nat st i in dom xp holds

xp . i = H

A12: dom xp = Seg (n + 1) by A10, FINSEQ_1:def 3;

A13: len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (n + 1) + 1 by CARD_1:def 7;

A14: for j being Nat st 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) holds

(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j

proof

Radix k > 0
by RADIX_2:6;
let j be Nat; :: thesis: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) implies (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j )

assume that

A15: 1 <= j and

A16: j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) ; :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j

j <= (n + 1) + 1 by A16, CARD_1:def 7;

then A17: j in Seg ((n + 1) + 1) by A15, FINSEQ_1:1;

A18: j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) by A15, A16, FINSEQ_3:25;

end;assume that

A15: 1 <= j and

A16: j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) ; :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j

j <= (n + 1) + 1 by A16, CARD_1:def 7;

then A17: j in Seg ((n + 1) + 1) by A15, FINSEQ_1:1;

A18: j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) by A15, A16, FINSEQ_3:25;

now :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . jend;

hence
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
; :: thesis: verumper cases
( j in Seg (n + 1) or j = (n + 1) + 1 )
by A17, FINSEQ_2:7;

end;

suppose A19:
j in Seg (n + 1)
; :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j

then
j in dom xp
by A10, FINSEQ_1:def 3;

then (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j = xp . j by FINSEQ_1:def 7

.= SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by A11, A12, A19

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. j by A17, Def11

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by A18, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j ; :: thesis: verum

end;then (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j = xp . j by FINSEQ_1:def 7

.= SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by A11, A12, A19

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. j by A17, Def11

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by A18, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j ; :: thesis: verum

suppose A20:
j = (n + 1) + 1
; :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j

A21:
j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))))
by A13, A17, FINSEQ_1:def 3;

(xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k) by A10, A20, FINSEQ_1:42

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. ((n + 1) + 1) by A17, A20, Def11

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by A20, A21, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j ; :: thesis: verum

end;(xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k) by A10, A20, FINSEQ_1:42

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. ((n + 1) + 1) by A17, A20, Def11

.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by A20, A21, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j ; :: thesis: verum

then x mod ((Radix k) |^ n) < (Radix k) |^ n by NAT_D:1, PREPOWER:6;

then x mod ((Radix k) |^ n) is_represented_by n,k ;

then A22: x mod ((Radix k) |^ n) = SDSub2IntOut (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) by A4, A6

.= Sum (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) ;

A23: n + 1 in Seg (n + 1) by FINSEQ_1:3;

then A24: n + 1 in Seg ((n + 1) + 1) by FINSEQ_2:8;

consider xpp being FinSequence of INT such that

A25: len xpp = n and

A26: for i being Nat st i in dom xpp holds

xpp . i = H

A27: dom xpp = Seg n by A25, FINSEQ_1:def 3;

A28: for j being Nat st 1 <= j & j <= len xp holds

xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j

proof

deffunc H
let j be Nat; :: thesis: ( 1 <= j & j <= len xp implies xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j )

assume ( 1 <= j & j <= len xp ) ; :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j

then A29: j in Seg (n + 1) by A10, FINSEQ_1:1;

end;assume ( 1 <= j & j <= len xp ) ; :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j

then A29: j in Seg (n + 1) by A10, FINSEQ_1:1;

now :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . jend;

hence
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
; :: thesis: verumper cases
( j in Seg n or j = n + 1 )
by A29, FINSEQ_2:7;

end;

suppose A30:
j in Seg n
; :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j

then
j in dom xpp
by A25, FINSEQ_1:def 3;

then (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j = xpp . j by FINSEQ_1:def 7

.= SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by A26, A27, A30

.= xp . j by A11, A12, A29 ;

hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum

end;then (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j = xpp . j by FINSEQ_1:def 7

.= SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by A26, A27, A30

.= xp . j by A11, A12, A29 ;

hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum

suppose A31:
j = n + 1
; :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j

then (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j =
SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k)
by A25, FINSEQ_1:42

.= xp . j by A11, A12, A29, A31 ;

hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum

end;.= xp . j by A11, A12, A29, A31 ;

hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum

consider xnpp being FinSequence of INT such that

A32: len xnpp = n and

A33: for i being Nat st i in dom xnpp holds

xnpp . i = H

A34: dom xnpp = Seg n by A32, FINSEQ_1:def 3;

for j being Nat st 1 <= j & j <= len xnpp holds

xnpp . j = xpp . j

proof

then A36:
xpp = xnpp
by A25, A32, FINSEQ_1:14;
let j be Nat; :: thesis: ( 1 <= j & j <= len xnpp implies xnpp . j = xpp . j )

assume ( 1 <= j & j <= len xnpp ) ; :: thesis: xnpp . j = xpp . j

then A35: j in Seg n by A32, FINSEQ_1:1;

then xpp . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by A26, A27

.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),j,k) by A6, A35, Th20

.= xnpp . j by A33, A34, A35 ;

hence xnpp . j = xpp . j ; :: thesis: verum

end;assume ( 1 <= j & j <= len xnpp ) ; :: thesis: xnpp . j = xpp . j

then A35: j in Seg n by A32, FINSEQ_1:1;

then xpp . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by A26, A27

.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),j,k) by A6, A35, Th20

.= xnpp . j by A33, A34, A35 ;

hence xnpp . j = xpp . j ; :: thesis: verum

A37: len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) = n + 1 by CARD_1:def 7;

A38: for j being Nat st 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) holds

(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j

proof

len xp = len (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>)
by A10, A25, FINSEQ_2:16;
let j be Nat; :: thesis: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) implies (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j )

assume A39: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) ) ; :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j

then A40: j in Seg (n + 1) by A37, FINSEQ_1:1;

A41: j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) by A39, FINSEQ_3:25;

end;assume A39: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) ) ; :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j

then A40: j in Seg (n + 1) by A37, FINSEQ_1:1;

A41: j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) by A39, FINSEQ_3:25;

now :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . jend;

hence
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
; :: thesis: verumper cases
( j in Seg n or j = n + 1 )
by A40, FINSEQ_2:7;

end;

suppose A42:
j in Seg n
; :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j

then
j in dom xnpp
by A32, FINSEQ_1:def 3;

then (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j = xnpp . j by FINSEQ_1:def 7

.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),j,k) by A33, A34, A42

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. j by A40, Def11

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j by A41, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j ; :: thesis: verum

end;then (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j = xnpp . j by FINSEQ_1:def 7

.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),j,k) by A33, A34, A42

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. j by A40, Def11

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j by A41, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j ; :: thesis: verum

suppose A43:
j = n + 1
; :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j

A44:
j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))))
by A37, A40, FINSEQ_1:def 3;

(xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k) by A32, A43, FINSEQ_1:42

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. (n + 1) by A40, A43, Def11

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j by A43, A44, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j ; :: thesis: verum

end;(xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k) by A32, A43, FINSEQ_1:42

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. (n + 1) by A40, A43, Def11

.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j by A43, A44, PARTFUN1:def 6 ;

hence (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j ; :: thesis: verum

then A45: xp = xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*> by A28, FINSEQ_1:14;

len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) = (n + 1) + 1 by A10, FINSEQ_2:16;

then len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) by CARD_1:def 7;

then SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))) = xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*> by A14, FINSEQ_1:14;

then A46: Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (Sum xp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k)) by RVSUM_1:74

.= ((Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k)) by A45, A36, RVSUM_1:74 ;

set RNDIG = ((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)));

set RNSDC = ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k));

A47: Radix k > 0 by RADIX_2:6;

len (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) = n + 1 by A32, FINSEQ_2:16;

then SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) = xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*> by A37, A38, FINSEQ_1:14;

then A48: (x mod ((Radix k) |^ n)) + 0 = (Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k)) by A22, RVSUM_1:74;

A49: SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k) = ((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) by NAT_D:34

.= ((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),(n + 1),k)) by A24, Def8

.= ((Radix k) |^ n) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),(n + 1),k)) by A6, A24, Def7

.= ((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))),k))) by A23, Def6

.= ((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NAT_D:34

.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))

.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NEWTON:6 ;

SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k) = ((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1))) by NAT_D:34

.= ((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k)) by A23, Def8

.= ((Radix k) |^ n) * (SD2SDSubDigit ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k)) by A23, A6, Def7

.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1))),k)) by Def6

.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)),k)) by NAT_D:34

.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)) by A5, Lm5 ;

then Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (((x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) - (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by A46, A48, A49, A9

.= (x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (x div ((Radix k) |^ n))) by A7, RADIX_1:24 ;

hence x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) by A47, NAT_D:2, PREPOWER:6; :: thesis: verum

proof

for n being Nat st n >= 1 holds
A51:
1 in Seg 1
by FINSEQ_1:1;

2 - 1 = 1 ;

then A52: 2 -' 1 = 1 by XREAL_0:def 2;

let k, x be Nat; :: thesis: ( k >= 2 & x is_represented_by 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k))) )

assume that

A53: k >= 2 and

A54: x is_represented_by 1,k ; :: thesis: x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k)))

set X = DecSD (x,1,k);

reconsider CRY = (Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) as Integer ;

reconsider DIG2 = CRY as Element of INT by INT_1:def 2;

reconsider DIG1 = (DigA ((DecSD (x,1,k)),1)) - CRY as Element of INT by INT_1:def 2;

A55: 1 in Seg (1 + 1) by FINSEQ_1:1;

A56: len (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) = 1 + 1 by CARD_1:def 7;

then A57: 1 in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) by A55, FINSEQ_1:def 3;

A58: 2 in Seg (1 + 1) by FINSEQ_1:1;

then A59: 2 in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) by A56, FINSEQ_1:def 3;

(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 2 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),2,k) by A58, Def11

.= (Radix k) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) by A52

.= (Radix k) * (SD2SDSubDigitS ((DecSD (x,1,k)),2,k)) by A58, Def8

.= (Radix k) * (SD2SDSubDigit ((DecSD (x,1,k)),2,k)) by A53, A58, Def7

.= (Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) by A52, A58, Def6 ;

then A60: (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 2 = CRY by A59, PARTFUN1:def 6;

(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 1 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),1,k) by A55, Def11

.= ((Radix k) |^ 0) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) by XREAL_1:232

.= 1 * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) by NEWTON:4

.= SD2SDSubDigitS ((DecSD (x,1,k)),1,k) by A55, Def8

.= SD2SDSubDigit ((DecSD (x,1,k)),1,k) by A53, A55, Def7

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),(1 -' 1))),k)) by A51, Def6

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),0)),k)) by XREAL_1:232

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def 3

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + 0 by Th16

.= (DigA ((DecSD (x,1,k)),1)) - ((Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k))) ;

then (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 1 = (DigA ((DecSD (x,1,k)),1)) - CRY by A57, PARTFUN1:def 6;

then SDSub2INT (SD2SDSub (DecSD (x,1,k))) = <*DIG1,DIG2*> by A56, A60, FINSEQ_1:44;

then Sum (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) = DIG1 + DIG2 by RVSUM_1:77

.= x by A54, RADIX_1:21 ;

hence x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k))) ; :: thesis: verum

end;2 - 1 = 1 ;

then A52: 2 -' 1 = 1 by XREAL_0:def 2;

let k, x be Nat; :: thesis: ( k >= 2 & x is_represented_by 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k))) )

assume that

A53: k >= 2 and

A54: x is_represented_by 1,k ; :: thesis: x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k)))

set X = DecSD (x,1,k);

reconsider CRY = (Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) as Integer ;

reconsider DIG2 = CRY as Element of INT by INT_1:def 2;

reconsider DIG1 = (DigA ((DecSD (x,1,k)),1)) - CRY as Element of INT by INT_1:def 2;

A55: 1 in Seg (1 + 1) by FINSEQ_1:1;

A56: len (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) = 1 + 1 by CARD_1:def 7;

then A57: 1 in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) by A55, FINSEQ_1:def 3;

A58: 2 in Seg (1 + 1) by FINSEQ_1:1;

then A59: 2 in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) by A56, FINSEQ_1:def 3;

(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 2 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),2,k) by A58, Def11

.= (Radix k) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) by A52

.= (Radix k) * (SD2SDSubDigitS ((DecSD (x,1,k)),2,k)) by A58, Def8

.= (Radix k) * (SD2SDSubDigit ((DecSD (x,1,k)),2,k)) by A53, A58, Def7

.= (Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) by A52, A58, Def6 ;

then A60: (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 2 = CRY by A59, PARTFUN1:def 6;

(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 1 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),1,k) by A55, Def11

.= ((Radix k) |^ 0) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) by XREAL_1:232

.= 1 * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) by NEWTON:4

.= SD2SDSubDigitS ((DecSD (x,1,k)),1,k) by A55, Def8

.= SD2SDSubDigit ((DecSD (x,1,k)),1,k) by A53, A55, Def7

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),(1 -' 1))),k)) by A51, Def6

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),0)),k)) by XREAL_1:232

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def 3

.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + 0 by Th16

.= (DigA ((DecSD (x,1,k)),1)) - ((Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k))) ;

then (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 1 = (DigA ((DecSD (x,1,k)),1)) - CRY by A57, PARTFUN1:def 6;

then SDSub2INT (SD2SDSub (DecSD (x,1,k))) = <*DIG1,DIG2*> by A56, A60, FINSEQ_1:44;

then Sum (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) = DIG1 + DIG2 by RVSUM_1:77

.= x by A54, RADIX_1:21 ;

hence x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k))) ; :: thesis: verum

S

hence for k, x being Nat st k >= 2 & x is_represented_by n,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k))) by A1; :: thesis: verum