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: 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 A2: for i being Nat st i in Seg 1 holds
DigA tx,i = DigA ty,i ; :: thesis: SDDec tx = SDDec ty
A3: 1 in Seg 1 by FINSEQ_1:3;
A4: SDDec tx = DigA tx,1 by Th4;
SDDec ty = DigA ty,1 by Th4;
hence SDDec tx = SDDec ty by A2, A3, A4; :: thesis: verum

end;

A5: 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 A6: ( n >= 1 & 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 A7: 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 K404() = DigB tx,$1;
consider txn being FinSequence of INT such that
A8: len txn = n and
A9: for i being Nat st i in dom txn holds
txn . i = H₁(i) from FINSEQ_2:sch 1();
A10: dom txn = Seg n by A8, 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
A11: xx in dom txn and
A12: z = txn . xx by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A11;
A13: dom txn = Seg n by A8, FINSEQ_1:def 3;
A14: z = DigB tx,xx by A9, A11, A12
.= DigA tx,xx by RADIX_1:def 4 ;
xx in Seg (n + 1) by A11, A13, FINSEQ_2:9;
then DigA tx,xx is Element of k -SD by RADIX_1:19;
hence z in k -SD by A14; :: thesis: verum

end;

then reconsider txn = txn as FinSequence of k -SD by FINSEQ_1:def 4;
A15: 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 A16: i in Seg n ; :: thesis: txn . i = tx . i
then A17: i in Seg (n + 1) by FINSEQ_2:9;
txn . i = DigB tx,i by A9, A16, A10
.= DigA tx,i by RADIX_1:def 4 ;
hence txn . i = tx . i by A17, RADIX_1:def 3; :: thesis: verum

end;

deffunc H₂( Nat) -> Element of K404() = DigB ty,$1;
consider tyn being FinSequence of INT such that
A18: len tyn = n and
A19: for i being Nat st i in dom tyn holds
tyn . i = H₂(i) from FINSEQ_2:sch 1();
A20: dom tyn = Seg n by A18, 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
A21: yy in dom tyn and
A22: z = tyn . yy by FUNCT_1:def 5;
reconsider yy = yy as Element of NAT by A21;
A23: dom tyn = Seg n by A18, FINSEQ_1:def 3;
A24: z = DigB ty,yy by A19, A21, A22
.= DigA ty,yy by RADIX_1:def 4 ;
yy in Seg (n + 1) by A21, A23, FINSEQ_2:9;
then DigA ty,yy is Element of k -SD by RADIX_1:19;
hence z in k -SD by A24; :: thesis: verum

end;

then reconsider tyn = tyn as FinSequence of k -SD by FINSEQ_1:def 4;
A25: 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 A26: i in Seg n ; :: thesis: tyn . i = ty . i
then A27: i in Seg (n + 1) by FINSEQ_2:9;
tyn . i = DigB ty,i by A19, A26, A20
.= DigA ty,i by RADIX_1:def 4 ;
hence tyn . i = ty . i by A27, RADIX_1:def 3; :: thesis: verum

end;

reconsider n = n as Element of NAT by ORDINAL1:def 13;
reconsider txn = txn as Tuple of n,(k -SD ) by A8, FINSEQ_2:110;
reconsider tyn = tyn as Tuple of n,(k -SD ) by A18, FINSEQ_2:110;
A28: (SDDec txn) + (((Radix k) |^ n) * (DigA tx,(n + 1))) = SDDec tx by A15, RADIX_2:10;
A29: (SDDec tyn) + (((Radix k) |^ n) * (DigA ty,(n + 1))) = SDDec ty by A25, RADIX_2:10;
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 A30: i in Seg n ; :: thesis: DigA txn,i = DigA tyn,i
then A31: DigA txn,i = txn . i by RADIX_1:def 3
.= DigB tx,i by A9, A30, A10
.= DigA tx,i by RADIX_1:def 4 ;
DigA tyn,i = tyn . i by A30, RADIX_1:def 3
.= DigB ty,i by A19, A30, A20
.= DigA ty,i by RADIX_1:def 4 ;
hence DigA txn,i = DigA tyn,i by A7, A30, A31, FINSEQ_2:9; :: thesis: verum

end;

then SDDec txn = SDDec tyn by A6;
hence SDDec tx = SDDec ty by A7, A28, A29, FINSEQ_1:6; :: thesis: verum

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A1, A5);
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