let f be real-valued FinSequence; :: thesis: for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds
ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
let n be Nat; :: thesis: ( card f = (n ^2) + 1 & f is one-to-one implies ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) )
assume that
A: card f = (n ^2) + 1 and
AA: f is one-to-one ; :: thesis: ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
set cP = f;
defpred S₁[ set , set ] means ex i, j being Nat ex r, s being real number st
( $1 = [i,r] & $2 = [j,s] & i < j & r < s );
consider iP being Relation of f,f such that
B: for x, y being set holds
( [x,y] in iP iff ( x in f & y in f & S₁[x,y] ) ) from RELSET_1:sch 1();
set P = RelStr(# f,iP #);
G3c: dom f = Seg (len f) by FINSEQ_1:def 3;
Pa: RelStr(# f,iP #) is antisymmetric

proof

let x, y be set ; :: according to RELAT_2:def 4,ORDERS_2:def 6 :: thesis: ( not x in the carrier of RelStr(# f,iP #) or not y in the carrier of RelStr(# f,iP #) or not [x,y] in the InternalRel of RelStr(# f,iP #) or not [y,x] in the InternalRel of RelStr(# f,iP #) or x = y )
assume that
x in the carrier of RelStr(# f,iP #) and
y in the carrier of RelStr(# f,iP #) and
C1: [x,y] in the InternalRel of RelStr(# f,iP #) and
D1: [y,x] in the InternalRel of RelStr(# f,iP #) ; :: thesis: x = y
consider i, j being Nat, r, s being real number such that
E1: x = [i,r] and
F1: y = [j,s] and
G1: ( i < j & r < s ) by C1, B;
consider j1, i1 being Nat, s1, r1 being real number such that
H1: y = [j1,s1] and
I1: x = [i1,r1] and
J1: ( j1 < i1 & s1 < r1 ) by D1, B;
( i = i1 & j = j1 ) by E1, F1, H1, I1, ZFMISC_1:33;
hence x = y by G1, J1; :: thesis: verum

end;

RelStr(# f,iP #) is transitive

proof

let x, y, z be set ; :: according to RELAT_2:def 8,ORDERS_2:def 5 :: thesis: ( not x in the carrier of RelStr(# f,iP #) or not y in the carrier of RelStr(# f,iP #) or not z in the carrier of RelStr(# f,iP #) or not [x,y] in the InternalRel of RelStr(# f,iP #) or not [y,z] in the InternalRel of RelStr(# f,iP #) or [x,z] in the InternalRel of RelStr(# f,iP #) )
assume that
A1: x in the carrier of RelStr(# f,iP #) and
y in the carrier of RelStr(# f,iP #) and
C1: z in the carrier of RelStr(# f,iP #) and
D1: [x,y] in the InternalRel of RelStr(# f,iP #) and
E1: [y,z] in the InternalRel of RelStr(# f,iP #) ; :: thesis: [x,z] in the InternalRel of RelStr(# f,iP #)
consider ix, jy being Nat, rx, sy being real number such that
F1: x = [ix,rx] and
G1: y = [jy,sy] and
H1: ( ix < jy & rx < sy ) by D1, B;
consider iy, jz being Nat, ry, sz being real number such that
I1: y = [iy,ry] and
J1: z = [jz,sz] and
K1: ( iy < jz & ry < sz ) by E1, B;
( jy = iy & sy = ry ) by G1, I1, ZFMISC_1:33;
then ( ix < jz & rx < sz ) by H1, K1, XXREAL_0:2;
hence [x,z] in the InternalRel of RelStr(# f,iP #) by F1, J1, A1, C1, B; :: thesis: verum

end;

then reconsider P = RelStr(# f,iP #) as finite transitive antisymmetric RelStr by Pa;
C: card P = card f ;

per cases ( ex C being Clique of P st card C >= n + 1 or ex A being StableSet of P st card A >= n + 1 ) by C, A, CSR;

suppose ex C being Clique of P st card C >= n + 1 ; :: thesis: ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )

then consider C being Clique of P such that
A1: card C >= n + 1 ;
set g = C;
reconsider g = C as Subset of f ;
reconsider g = g as Function ;
dom g c= Seg (len f)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in Seg (len f) )
assume x in dom g ; :: thesis: x in Seg (len f)
then consider y being set such that
A2: [x,y] in g by RELAT_1:def 4;
x in dom f by A2, RELAT_1:def 4;
hence x in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

end;

then reconsider g = g as FinSubsequence by FINSEQ_1:def 12;
reconsider g = g as real-valued FinSubsequence ;
take g ; :: thesis: ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus g c= f ; :: thesis: ( card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus card g >= n + 1 by A1; :: thesis: ( g is increasing or g is decreasing )
g is increasing

proof

let e1, e2 be ext-real number ; :: according to VALUED_0:def 13 :: thesis: ( not e1 in proj1 g or not e2 in proj1 g or e2 <= e1 or not g . e2 <= g . e1 )
assume that
A3: e1 in dom g and
B3: e2 in dom g and
C3: e1 < e2 ; :: thesis: not g . e2 <= g . e1
D3: [e1,(g . e1)] in g by A3, FUNCT_1:8;
E3: [e2,(g . e2)] in g by B3, FUNCT_1:8;
then reconsider p1 = [e1,(g . e1)], p2 = [e2,(g . e2)] as Element of P by D3;
F3: p1 <> p2 by C3, ZFMISC_1:33;

per cases ( p1 <= p2 or p2 <= p1 ) by D3, E3, F3, DClique;

suppose p1 <= p2 ; :: thesis: not g . e2 <= g . e1

then [p1,p2] in iP by ORDERS_2:def 9;
then consider i, j being Nat, r, s being real number such that
A4: p1 = [i,r] and
B4: p2 = [j,s] and
C4: ( i < j & r < s ) by B;
( j = e2 & s = g . e2 ) by B4, ZFMISC_1:33;
hence g . e1 < g . e2 by C4, A4, ZFMISC_1:33; :: thesis: verum

end;

suppose p2 <= p1 ; :: thesis: not g . e2 <= g . e1

then [p2,p1] in iP by ORDERS_2:def 9;
then consider i, j being Nat, r, s being real number such that
A4: p2 = [i,r] and
B4: p1 = [j,s] and
C4: ( i < j & r < s ) by B;
( i = e2 & j = e1 ) by A4, B4, ZFMISC_1:33;
hence g . e1 < g . e2 by C3, C4; :: thesis: verum

end;

end;

end;

hence ( g is increasing or g is decreasing ) ; :: thesis: verum

end;

suppose ex A being StableSet of P st card A >= n + 1 ; :: thesis: ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )

then consider A being StableSet of P such that
A1: card A >= n + 1 ;
set g = A;
reconsider g = A as Subset of f ;
reconsider g = g as Function ;
B1: dom g c= Seg (len f)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in Seg (len f) )
assume x in dom g ; :: thesis: x in Seg (len f)
then consider y being set such that
A2: [x,y] in g by RELAT_1:def 4;
x in dom f by A2, RELAT_1:def 4;
hence x in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

end;

then reconsider g = g as FinSubsequence by FINSEQ_1:def 12;
reconsider g = g as real-valued FinSubsequence ;
take g ; :: thesis: ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus g c= f ; :: thesis: ( card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus card g >= n + 1 by A1; :: thesis: ( g is increasing or g is decreasing )
g is decreasing

proof

let e1, e2 be ext-real number ; :: according to VALUED_0:def 14 :: thesis: ( not e1 in proj1 g or not e2 in proj1 g or e2 <= e1 or not g . e1 <= g . e2 )
assume that
A3: e1 in dom g and
B3: e2 in dom g and
C3: e1 < e2 ; :: thesis: not g . e1 <= g . e2
D3: [e1,(g . e1)] in g by A3, FUNCT_1:8;
E3: [e2,(g . e2)] in g by B3, FUNCT_1:8;
then reconsider p1 = [e1,(g . e1)], p2 = [e2,(g . e2)] as Element of P by D3;
F3: p1 <> p2 by C3, ZFMISC_1:33;
( g . e1 = f . e1 & g . e2 = f . e2 ) by A3, B3, GRFUNC_1:8;
then G3: g . e1 <> g . e2 by G3c, B1, A3, B3, C3, AA, FUNCT_1:def 8;
reconsider i = e1, j = e2 as Nat by B1, A3, B3;
reconsider r = g . e1, s = g . e2 as real number ;
H3: ( p1 = [i,r] & p2 = [j,s] ) ;

per cases ( g . e1 < g . e2 or g . e1 > g . e2 ) by G3, XXREAL_0:1;

suppose g . e1 < g . e2 ; :: thesis: not g . e1 <= g . e2

then [p1,p2] in iP by D3, B, C3, H3;
then p1 <= p2 by ORDERS_2:def 9;
hence g . e1 > g . e2 by D3, E3, F3, LAChain; :: thesis: verum

end;

suppose g . e1 > g . e2 ; :: thesis: not g . e1 <= g . e2

hence not g . e1 <= g . e2 ; :: thesis: verum

end;

end;

end;

hence ( g is increasing or g is decreasing ) ; :: thesis: verum

end;

end;