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:5;
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 13;
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:5;
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 FINSEQ_1:def 18;
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, FINSEQ_1:def 18;
then A17: j in Seg ((n + 1) + 1) by A15, FINSEQ_1:3;
A18: j in dom (SDSub2INT (SD2SDSub (DecSD x,(n + 1),k))) by A15, A16, FINSEQ_3:27;
now
per cases ( j in Seg (n + 1) or j = (n + 1) + 1 ) by A17, FINSEQ_2:8;
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 8 ;
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:59
.= (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 8 ;
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:13;
then x mod ((Radix k) |^ n) is_represented_by n,k by RADIX_1:def 12;
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:5;
then A24: n + 1 in Seg ((n + 1) + 1) by FINSEQ_2:9;
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:3;
now
per cases ( j in Seg n or j = n + 1 ) by A29, FINSEQ_2:8;
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:59
.= 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:3;
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, Th21
.= xnpp . j by A33, A34, A35 ;
hence xnpp . j = xpp . j ; :: thesis: verum
end;
then A36: xpp = xnpp by A25, A32, FINSEQ_1:18;
A37: len (SDSub2INT (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k))) = n + 1 by FINSEQ_1:def 18;
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:3;
A41: j in dom (SDSub2INT (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k))) by A39, FINSEQ_3:27;
now
per cases ( j in Seg n or j = n + 1 ) by A40, FINSEQ_2:8;
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 8 ;
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:59
.= (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 8 ;
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:19;
then A45: xp = xpp ^ <*(SDSub2INTDigit (SD2SDSub (DecSD x,(n + 1),k)),(n + 1),k)*> by A28, FINSEQ_1:18;
len (xp ^ <*(SDSub2INTDigit (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1),k)*>) = (n + 1) + 1 by A10, FINSEQ_2:19;
then len (SDSub2INT (SD2SDSub (DecSD x,(n + 1),k))) = len (xp ^ <*(SDSub2INTDigit (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1),k)*>) by FINSEQ_1:def 18;
then SDSub2INT (SD2SDSub (DecSD x,(n + 1),k)) = xp ^ <*(SDSub2INTDigit (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1),k)*> by A14, FINSEQ_1:18;
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:104
.= ((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:104 ;
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:19;
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:18;
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:104;
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:11 ;
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:27 ;
hence x = SDSub2IntOut (SD2SDSub (DecSD x,(n + 1),k)) by A47, NAT_D:2, PREPOWER:13; :: thesis: verum
end;
A50: S1[1]
proof
A51: 1 in Seg 1 by FINSEQ_1:3;
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:3;
A56: len (SDSub2INT (SD2SDSub (DecSD x,1,k))) = 1 + 1 by FINSEQ_1:def 18;
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:3;
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, NEWTON:10
.= (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 8;
(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:234
.= 1 * (DigB_SDSub (SD2SDSub (DecSD x,1,k)),1) by NEWTON:9
.= 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:234
.= (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 Th17
.= (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 8;
then SDSub2INT (SD2SDSub (DecSD x,1,k)) = <*DIG1,DIG2*> by A56, A60, FINSEQ_1:61;
then Sum (SDSub2INT (SD2SDSub (DecSD x,1,k))) = DIG1 + DIG2 by RVSUM_1:107
.= x by A54, RADIX_1:24 ;
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