defpred S1[ 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 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A3: n >= 1 and
A4: S1[n] ; :: thesis: S1[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 H1( 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 = H1(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
proof
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;
now :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
per cases ( j in Seg (n + 1) or j = (n + 1) + 1 ) by A17, FINSEQ_2:7;
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;
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;
end;
end;
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;
Radix k > 0 by RADIX_2:6;
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 = H1(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
proof
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;
now :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
per cases ( j in Seg n or j = n + 1 ) by A29, FINSEQ_2:7;
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;
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;
end;
end;
hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum
end;
deffunc H2( 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 = H2(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
proof
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;
then A36: xpp = xnpp by A25, A32, FINSEQ_1:14;
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
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;
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))*>) . j
per cases ( j in Seg n or j = n + 1 ) by A40, FINSEQ_2:7;
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;
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;
end;
end;
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;
len xp = len (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) by A10, A25, FINSEQ_2:16;
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;
A50: S1[1]
proof
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;
for n being Nat st n >= 1 holds
S1[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