defpred S1[ 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 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1 and
A2: S1[n] ; :: thesis: S1[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 12;
deffunc H1( Nat) -> Element of INT = 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 = H1(i) from FINSEQ_2:sch 1();
 deffunc H2( Nat) -> Element of INT = 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 = H2(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 object ; :: 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 object such that
A9: yy in dom tyn and
A10: z = tyn . yy by FUNCT_1:def 3;
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:8;
then A11: DigA (ty,yy) is Element of k -SD by RADIX_1:16;
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:8;
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:92;
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 object ; :: 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 object such that
A16: xx in dom txn and
A17: z = txn . xx by FUNCT_1:def 3;
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:8;
then A18: DigA (tx,xx) is Element of k -SD by RADIX_1:16;
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:8;
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: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 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:8; :: thesis: verum
end;
then A24: SDDec txn >= SDDec tyn by A2;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A25: ((Radix k) |^ n) * (DigA (tx,(n + 1))) >= ((Radix k) |^ n) * (DigA (ty,(n + 1))) by A3, XREAL_1:64;
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:7; :: thesis: verum
end;
A27: S1[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:1;
hence SDDec tx >= SDDec ty by A28, A29; :: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[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