let R be non empty RelStr ; :: thesis: ( R is Dickson implies for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j ) )
assume A1: R is Dickson ; :: thesis: for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j )
let f be sequence of R; :: thesis: ex i, j being Nat st
( i < j & f . i <= f . j )
set N = rng f;
A2: dom f = NAT by FUNCT_2:def 1;
consider B being set such that
A3: B is_Dickson-basis_of rng f,R and
A4: B is finite by A1;
reconsider B = B as non empty finite set by A3, A4, Th25;
defpred S₁[ set ] means verum;
deffunc H₁( set ) -> Element of NAT = f mindex $1;
set BI = { H₁(b) where b is Element of B : S₁[b] } ;
A5: { H₁(b) where b is Element of B : S₁[b] } is finite from PRE_CIRC:sch 1();
set b = the Element of B;
A6: f mindex the Element of B in { H₁(b) where b is Element of B : S₁[b] } ;

now :: thesis: for x being object st x in { H₁(b) where b is Element of B : S₁[b] } holds
x in NAT

let x be object ; :: thesis: ( x in { H₁(b) where b is Element of B : S₁[b] } implies x in NAT )
assume x in { H₁(b) where b is Element of B : S₁[b] } ; :: thesis: x in NAT
then ex b being Element of B st x = f mindex b ;
hence x in NAT ; :: thesis: verum

end;

then reconsider BI = { H₁(b) where b is Element of B : S₁[b] } as non empty finite Subset of NAT by A5, A6, TARSKI:def 3;
reconsider mB = max BI as Element of NAT by ORDINAL1:def 12;
set j = mB + 1;
reconsider fj = f . (mB + 1) as Element of R ;
fj in rng f by A2, FUNCT_1:3;
then consider b being Element of R such that
A7: b in B and
A8: b <= fj by A3;
A9: B c= rng f by A3;
take i = f mindex b; :: thesis: ex j being Nat st
( i < j & f . i <= f . j )
take mB + 1 ; :: thesis: ( i < mB + 1 & f . i <= f . (mB + 1) )
i in BI by A7;
then i <= max BI by XXREAL_2:def 8;
hence i < mB + 1 by NAT_1:13; :: thesis: f . i <= f . (mB + 1)
dom f = NAT by NORMSP_1:12;
hence f . i <= f . (mB + 1) by A7, A8, A9, Def11; :: thesis: verum