defpred S₁[ Nat] means for k being Nat
for tx, ty being Tuple of $1,k -SD st ( for i being Nat st i in Seg $1 holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty;
A1: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume that
n >= 1 and
A2: S₁[n] ; :: thesis: S₁[n + 1]
let k be Nat; :: thesis: for tx, ty being Tuple of n + 1,k -SD st ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty
let tx, ty be Tuple of n + 1,k -SD ; :: thesis: ( ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) = DigA (ty,i) ) implies SDDec tx = SDDec ty )
assume A3: for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) = DigA (ty,i) ; :: thesis: SDDec tx = SDDec ty
deffunc H₁( Nat) -> Element of K367() = DigB (tx,$1);
consider txn being FinSequence of INT such that
A4: len txn = n and
A5: for i being Nat st i in dom txn holds
txn . i = H₁(i) from FINSEQ_2:sch 1();
A6: dom txn = Seg n by A4, FINSEQ_1:def 3;
rng txn c= k -SD

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng txn or z in k -SD )
assume z in rng txn ; :: thesis: z in k -SD
then consider xx being set such that
A7: xx in dom txn and
A8: z = txn . xx by FUNCT_1:def 3;
reconsider xx = xx as Element of NAT by A7;
dom txn = Seg n by A4, FINSEQ_1:def 3;
then xx in Seg (n + 1) by A7, FINSEQ_2:8;
then A9: DigA (tx,xx) is Element of k -SD by RADIX_1:16;
z = DigB (tx,xx) by A5, A7, A8
.= DigA (tx,xx) by RADIX_1:def 4 ;
hence z in k -SD by A9; :: thesis: verum

end;

then reconsider txn = txn as FinSequence of k -SD by FINSEQ_1:def 4;
A10: for i being Nat st i in Seg n holds
txn . i = tx . i

proof

let i be Nat; :: thesis: ( i in Seg n implies txn . i = tx . i )
assume A11: i in Seg n ; :: thesis: txn . i = tx . i
then A12: i in Seg (n + 1) by FINSEQ_2:8;
txn . i = DigB (tx,i) by A5, A6, A11
.= DigA (tx,i) by RADIX_1:def 4 ;
hence txn . i = tx . i by A12, RADIX_1:def 3; :: thesis: verum

end;

deffunc H₂( Nat) -> Element of K367() = DigB (ty,$1);
consider tyn being FinSequence of INT such that
A13: len tyn = n and
A14: for i being Nat st i in dom tyn holds
tyn . i = H₂(i) from FINSEQ_2:sch 1();
A15: dom tyn = Seg n by A13, FINSEQ_1:def 3;
rng tyn c= k -SD

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng tyn or z in k -SD )
assume z in rng tyn ; :: thesis: z in k -SD
then consider yy being set such that
A16: yy in dom tyn and
A17: z = tyn . yy by FUNCT_1:def 3;
reconsider yy = yy as Element of NAT by A16;
dom tyn = Seg n by A13, FINSEQ_1:def 3;
then yy in Seg (n + 1) by A16, FINSEQ_2:8;
then A18: DigA (ty,yy) is Element of k -SD by RADIX_1:16;
z = DigB (ty,yy) by A14, A16, A17
.= DigA (ty,yy) by RADIX_1:def 4 ;
hence z in k -SD by A18; :: thesis: verum

end;

then reconsider tyn = tyn as FinSequence of k -SD by FINSEQ_1:def 4;
A19: for i being Nat st i in Seg n holds
tyn . i = ty . i

proof

let i be Nat; :: thesis: ( i in Seg n implies tyn . i = ty . i )
assume A20: i in Seg n ; :: thesis: tyn . i = ty . i
then A21: i in Seg (n + 1) by FINSEQ_2:8;
tyn . i = DigB (ty,i) by A14, A15, A20
.= DigA (ty,i) by RADIX_1:def 4 ;
hence tyn . i = ty . i by A21, RADIX_1:def 3; :: thesis: verum

end;

reconsider n = n as Element of NAT by ORDINAL1:def 12;
tyn is Element of n -tuples_on (k -SD) by A13, FINSEQ_2:92;
then reconsider tyn = tyn as Tuple of n,k -SD ;
A22: (SDDec tyn) + (((Radix k) |^ n) * (DigA (ty,(n + 1)))) = SDDec ty by A19, RADIX_2:10;
txn is Element of n -tuples_on (k -SD) by A4, FINSEQ_2:92;
then reconsider txn = txn as Tuple of n,k -SD ;
for i being Nat st i in Seg n holds
DigA (txn,i) = DigA (tyn,i)

proof

let i be Nat; :: thesis: ( i in Seg n implies DigA (txn,i) = DigA (tyn,i) )
assume A23: i in Seg n ; :: thesis: DigA (txn,i) = DigA (tyn,i)
then A24: DigA (tyn,i) = tyn . i by RADIX_1:def 3
.= DigB (ty,i) by A14, A15, A23
.= DigA (ty,i) by RADIX_1:def 4 ;
DigA (txn,i) = txn . i by A23, RADIX_1:def 3
.= DigB (tx,i) by A5, A6, A23
.= DigA (tx,i) by RADIX_1:def 4 ;
hence DigA (txn,i) = DigA (tyn,i) by A3, A23, A24, FINSEQ_2:8; :: thesis: verum

end;

then A25: SDDec txn = SDDec tyn by A2;
(SDDec txn) + (((Radix k) |^ n) * (DigA (tx,(n + 1)))) = SDDec tx by A10, RADIX_2:10;
hence SDDec tx = SDDec ty by A3, A22, A25, FINSEQ_1:4; :: thesis: verum

end;

A26: S₁[1]

proof

let k be Nat; :: thesis: for tx, ty being Tuple of 1,k -SD st ( for i being Nat st i in Seg 1 holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty
let tx, ty be Tuple of 1,k -SD ; :: thesis: ( ( for i being Nat st i in Seg 1 holds
DigA (tx,i) = DigA (ty,i) ) implies SDDec tx = SDDec ty )
assume A27: for i being Nat st i in Seg 1 holds
DigA (tx,i) = DigA (ty,i) ; :: thesis: SDDec tx = SDDec ty
A28: SDDec ty = DigA (ty,1) by Th4;
( 1 in Seg 1 & SDDec tx = DigA (tx,1) ) by Th4, FINSEQ_1:1;
hence SDDec tx = SDDec ty by A27, A28; :: thesis: verum

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A26, A1);
hence for n being Nat st n >= 1 holds
for k being Nat
for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty ; :: thesis: verum