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

end;

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

end;

tyn is Element of n -tuples_on (k -SD ) by A6, FINSEQ_2:110;
then reconsider tyn = tyn as Tuple of n,k -SD ;
A15: 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
A16: xx in dom txn and
A17: z = txn . xx by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A16;
dom txn = Seg n by A4, FINSEQ_1:def 3;
then xx in Seg (n + 1) by A16, FINSEQ_2:9;
then A18: DigA tx,xx is Element of k -SD by RADIX_1:19;
z = DigB tx,xx by A5, A16, A17
.= DigA tx,xx by RADIX_1:def 4 ;
hence z in k -SD by A18; :: thesis: verum

end;

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

end;

txn is Element of n -tuples_on (k -SD ) by A4, FINSEQ_2:110;
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 A22: i in Seg n ; :: thesis: DigA txn,i >= DigA tyn,i
then A23: DigA tyn,i = tyn . i by RADIX_1:def 3
.= DigB ty,i by A7, A8, A22
.= DigA ty,i by RADIX_1:def 4 ;
DigA txn,i = txn . i by A22, RADIX_1:def 3
.= DigB tx,i by A5, A15, A22
.= DigA tx,i by RADIX_1:def 4 ;
hence DigA txn,i >= DigA tyn,i by A3, A22, A23, FINSEQ_2:9; :: thesis: verum

end;

then A24: SDDec txn >= SDDec tyn by A2;
n + 1 in Seg (n + 1) by FINSEQ_1:6;
then A25: ((Radix k) |^ n) * (DigA tx,(n + 1)) >= ((Radix k) |^ n) * (DigA ty,(n + 1)) by A3, XREAL_1:66;
A26: (SDDec tyn) + (((Radix k) |^ n) * (DigA ty,(n + 1))) = SDDec ty by A12, RADIX_2:10;
(SDDec txn) + (((Radix k) |^ n) * (DigA tx,(n + 1))) = SDDec tx by A19, RADIX_2:10;
hence SDDec tx >= SDDec ty by A26, A24, A25, XREAL_1:9; :: thesis: verum

end;

A27: 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 A28: for i being Nat st i in Seg 1 holds
DigA tx,i >= DigA ty,i ; :: thesis: SDDec tx >= SDDec ty
A29: SDDec ty = DigA ty,1 by Th4;
( 1 in Seg 1 & SDDec tx = DigA tx,1 ) by Th4, FINSEQ_1:3;
hence SDDec tx >= SDDec ty by A28, A29; :: thesis: verum

end;

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