let R be non empty RelStr ; for s being sequence of R st R is Dickson holds
ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending )
let s be sequence of R; ( R is Dickson implies ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending ) )
assume A1:
R is Dickson
; ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending )
set CR = the carrier of R;
deffunc H1( Element of rng s, Element of NAT ) -> set = { n where n is Element of NAT : ( $1 <= s . n & $2 < n ) } ;
deffunc H2( Element of rng s) -> set = { n where n is Element of NAT : $1 <= s . n } ;
defpred S1[ set , Element of NAT , set ] means ex N being Subset of the carrier of R ex B being non empty Subset of the carrier of R st
( N = { (s . w) where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } & { w where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & $3 = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,$2) is infinite ) } ,$2) );
defpred S2[ set , Element of NAT , set ] means ( { w where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } is infinite implies S1[$1,$2,$3] );
A2:
for n being Nat
for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n be
Nat;
for x being Element of NAT ex y being Element of NAT st S2[n,x,y]let x be
Element of
NAT ;
ex y being Element of NAT st S2[n,x,y]
set N =
{ (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
then reconsider N =
{ (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } as
Subset of the
carrier of
R by TARSKI:def 3;
set W =
{ w where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
per cases
( N is empty or not N is empty )
;
suppose A7:
not
N is
empty
;
ex y being Element of NAT st S2[n,x,y]set BBX =
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } ;
set B = the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } ;
consider BD1 being
set such that A8:
BD1 is_Dickson-basis_of N,
R
and A9:
BD1 is
finite
by A1;
BD1 in Dickson-bases (
N,
R)
by A1, A8, Def13;
then
BD1 in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
by A9;
then
the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
;
then
ex
BBB being
Element of
Dickson-bases (
N,
R) st
( the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } = BBB &
BBB is
finite )
;
then A10:
the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } is_Dickson-basis_of N,
R
by A1, Def13;
reconsider B = the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } as non
empty Subset of the
carrier of
R by A7, A10, Th25, XBOOLE_1:1;
set y =
s mindex ( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,
x);
take
s mindex ( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,
x)
;
S2[n,x,s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x)]set W =
{ w where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
assume A11:
{ w where w is Element of NAT : ( s . x <= s . w & x < w ) } is
infinite
;
S1[n,x,s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x)]take
N
;
ex B being non empty Subset of the carrier of R st
( N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } & { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) )reconsider B =
B as non
empty Subset of the
carrier of
R ;
take
B
;
( N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } & { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) )thus
N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) }
;
( { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) )thus
{ w where w is Element of NAT : ( s . x <= s . w & x < w ) } is
infinite
by A11;
( B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) )thus
B = the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite }
;
s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x)thus
s mindex ( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,
x)
= s mindex ( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,
x)
;
verum end; end;
end;
consider B being set such that
A12:
B is_Dickson-basis_of rng s,R
and
A13:
B is finite
by A1;
reconsider B = B as non empty set by A12, Th25;
set BALL = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } ;
set b1 = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } ;
consider f being sequence of NAT such that
A14:
f . 0 = s mindex the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) }
and
A15:
for n being Nat holds S2[n,f . n,f . (n + 1)]
from RECDEF_1:sch 2(A2);
A16:
dom f = NAT
by FUNCT_2:def 1;
A17:
rng f c= NAT
;
then consider tb being Element of rng s such that
A26:
tb in B
and
A27:
H2(tb) is infinite
;
A28:
tb in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) }
by A26, A27;
then
the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) }
;
then A29:
ex bt being Element of B st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } = bt & ex b9 being Element of rng s st
( b9 = bt & H2(b9) is infinite ) )
;
dom s = NAT
by NORMSP_1:12;
then A30:
s . (f . 0) = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) }
by A14, A29, Def11;
the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) }
by A28;
then A31:
ex eb being Element of B st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } = eb & ex eb9 being Element of rng s st
( eb9 = eb & H2(eb9) is infinite ) )
;
deffunc H3( set ) -> set = $1;
defpred S3[ Nat] means ( 0 <= $1 & s . (f . 0) <= s . $1 );
set W1 = { w where w is Element of NAT : s . (f . 0) <= s . w } ;
set W2 = { w where w is Element of NAT : ( s . (f . 0) <= s . w & f . 0 < w ) } ;
set W3 = { H3(w) where w is Nat : ( w <= f . 0 & S3[w] ) } ;
A32:
{ H3(w) where w is Nat : ( w <= f . 0 & S3[w] ) } is finite
from FINSEQ_1:sch 6();
then A38:
{ w where w is Element of NAT : ( s . (f . 0) <= s . w & f . 0 < w ) } is infinite
by A30, A31, A32, TARSKI:2;
defpred S4[ Nat] means S1[$1,f . $1,f . ($1 + 1)];
A39:
S4[ 0 ]
by A15, A38;
A40:
now for k being Nat st S4[k] holds
S4[k + 1]let k be
Nat;
( S4[k] implies S4[k + 1] )assume
S4[
k]
;
S4[k + 1]then consider N being
Subset of the
carrier of
R,
B being non
empty Subset of the
carrier of
R such that A41:
N = { (s . w) where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) }
and A42:
{ w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } is
infinite
and A43:
B = the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite }
and A44:
f . (k + 1) = s mindex ( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } ,
(f . k))
;
set BALL =
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } ;
set BBX =
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } ;
set iN =
{ w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } ;
consider BD being
set such that A45:
BD is_Dickson-basis_of N,
R
and A46:
BD is
finite
by A1;
BD in Dickson-bases (
N,
R)
by A1, A45, Def13;
then
BD in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
by A46;
then
B in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
by A43;
then A47:
ex
BB being
Element of
Dickson-bases (
N,
R) st
(
B = BB &
BB is
finite )
;
then A48:
B is_Dickson-basis_of N,
R
by A1, Def13;
then consider b being
Element of
rng s such that A62:
b in B
and A63:
H1(
b,
f . k) is
infinite
;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) }
by A62, A63;
then
the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) }
;
then consider b being
Element of
B such that A64:
b = the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) }
and A65:
ex
b9 being
Element of
rng s st
(
b9 = b &
H1(
b9,
f . k) is
infinite )
;
B c= N
by A48;
then
b in N
;
then A66:
ex
w being
Element of
NAT st
(
b = s . w &
s . (f . k) <= s . w &
f . k < w )
by A41;
then A67:
s . (f . (k + 1)) = the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) }
by A44, A64, Def12;
A68:
f . k < f . (k + 1)
by A44, A64, A66, Def12;
deffunc H4(
set )
-> set = $1;
defpred S5[
Nat]
means (
f . k < $1 &
s . (f . (k + 1)) <= s . $1 );
set W1 =
{ w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } ;
set W2 =
{ w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } ;
set W3 =
{ H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } ;
A69:
{ H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } is
finite
from FINSEQ_1:sch 6();
now for x being object holds
( ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } implies x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } ) & ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } implies x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } ) )let x be
object ;
( ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } implies x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } ) & ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } implies b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) } ) )hereby ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } implies b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) } )
end; assume A73:
x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) }
;
b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) } end; then
{ w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } is
infinite
by A64, A65, A67, A69, TARSKI:2;
hence
S4[
k + 1]
by A15;
verum end;
A78:
for n being Nat holds S4[n]
from NAT_1:sch 2(A39, A40);
set t = s * f;
take
s * f
; ( s * f is subsequence of s & s * f is weakly-ascending )
reconsider f = f as sequence of REAL by FUNCT_2:7, NUMBERS:19;
now ( f is increasing & ( for n being Element of NAT holds f . n is Element of NAT ) )now for n being Nat holds f . n < f . (n + 1)let n be
Nat;
f . n < f . (n + 1)A79:
n in NAT
by ORDINAL1:def 12;
f . n in rng f
by A16, A79, FUNCT_1:def 3;
then reconsider fn =
f . n as
Element of
NAT by A17;
consider N being
Subset of the
carrier of
R,
B being non
empty Subset of the
carrier of
R such that A80:
N = { (s . w) where w is Element of NAT : ( s . fn <= s . w & fn < w ) }
and A81:
{ w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } is
infinite
and A82:
B = the
Element of
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite }
and A83:
f . (n + 1) = s mindex ( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } ,
fn)
by A78;
set BBX =
{ BB where BB is Element of Dickson-bases (N,R) : BB is finite } ;
set BJ =
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } ;
set BC = the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } ;
consider BD being
set such that A84:
BD is_Dickson-basis_of N,
R
and A85:
BD is
finite
by A1;
BD in Dickson-bases (
N,
R)
by A1, A84, Def13;
then
BD in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
by A85;
then
B in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
by A82;
then A86:
ex
BB being
Element of
Dickson-bases (
N,
R) st
(
B = BB &
BB is
finite )
;
then A87:
B is_Dickson-basis_of N,
R
by A1, Def13;
then A88:
B c= N
;
then consider b being
Element of
rng s such that A102:
b in B
and A103:
H1(
b,
fn) is
infinite
;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) }
by A102, A103;
then
the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) }
;
then
ex
b being
Element of
B st
( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } = b & ex
b9 being
Element of
rng s st
(
b9 = b &
H1(
b9,
fn) is
infinite ) )
;
then
the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } in N
by A88;
then
ex
j being
Element of
NAT st
( the
Element of
{ b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } = s . j &
s . fn <= s . j &
fn < j )
by A80;
hence
f . n < f . (n + 1)
by A83, Def12;
verum end; hence
f is
increasing
by SEQM_3:def 6;
for n being Element of NAT holds f . n is Element of NAT let n be
Element of
NAT ;
f . n is Element of NAT
f . n in rng f
by A16, FUNCT_1:def 3;
hence
f . n is
Element of
NAT
by A17;
verum end;
then reconsider f = f as increasing sequence of NAT ;
s * f = s * f
;
hence
s * f is subsequence of s
; s * f is weakly-ascending
let n be Nat; DICKSON:def 2 [((s * f) . n),((s * f) . (n + 1))] in the InternalRel of R
n in NAT
by ORDINAL1:def 12;
then A104:
(s * f) . n = s . (f . n)
by A16, FUNCT_1:13;
A105:
(s * f) . (n + 1) = s . (f . (n + 1))
by A16, FUNCT_1:13;
consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A106:
N = { (s . w) where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) }
and
A107:
{ w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } is infinite
and
A108:
B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
and
A109:
f . (n + 1) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } ,(f . n))
by A78;
set BX = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } ;
set sfn1 = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } ;
set BBX = { BB where BB is Element of Dickson-bases (N,R) : BB is finite } ;
consider BD being set such that
A110:
BD is_Dickson-basis_of N,R
and
A111:
BD is finite
by A1;
BD in Dickson-bases (N,R)
by A1, A110, Def13;
then
BD in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
by A111;
then
B in { BB where BB is Element of Dickson-bases (N,R) : BB is finite }
by A108;
then A112:
ex BB being Element of Dickson-bases (N,R) st
( BB = B & BB is finite )
;
then A113:
B is_Dickson-basis_of N,R
by A1, Def13;
then consider b being Element of rng s such that
A127:
b in B
and
A128:
H1(b,f . n) is infinite
;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) }
by A127, A128;
then
the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) }
;
then
ex b being Element of B st
( b = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } & ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) )
;
then A129:
the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } in B
;
B c= N
by A113;
then
the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } in N
by A129;
then
ex w being Element of NAT st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } = s . w & s . (f . n) <= s . w & f . n < w )
by A106;
then
(s * f) . n <= (s * f) . (n + 1)
by A104, A105, A109, Def12;
hence
[((s * f) . n),((s * f) . (n + 1))] in the InternalRel of R
; verum