let R be non empty RelStr ; :: thesis: ( R is Dickson implies for f being sequence of R ex i, j being Element of NAT st
( i < j & f . i <= f . j ) )
assume A1: R is Dickson ; :: thesis: for f being sequence of R ex i, j being Element of NAT st
( i < j & f . i <= f . j )
let f be sequence of R; :: thesis: ex i, j being Element of 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, Def10;
reconsider B = B as non empty finite set by A3, A4, Th27;
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();
consider b being Element of B;
A6: f mindex b in { H₁(b) where b is Element of B : S₁[b] } ;

now

let x be set ; :: 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 13;
set j = mB + 1;
reconsider fj = f . (mB + 1) as Element of R ;
fj in rng f by A2, FUNCT_1:12;
then consider b being Element of R such that
A7: b in B and
A8: b <= fj by A3, Def9;
A9: B c= rng f by A3, Def9;
take i = f mindex b; :: thesis: ex j being Element of 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:17;
hence f . i <= f . (mB + 1) by A7, A8, A9, Def11; :: thesis: verum