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
A1: card f = (n ^2) + 1 and
A2: 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₁[ object , object ] means ex i, j being Nat ex r, s being Real st
( $1 = [i,r] & $2 = [j,s] & i < j & r < s );
consider iP being Relation of f,f such that
A3: for x, y being object 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 #);
A4: dom f = Seg (len f) by FINSEQ_1:def 3;
A5: RelStr(# f,iP #) is antisymmetric

proof

let x, y be object ; :: according to RELAT_2:def 4,ORDERS_2:def 4 :: 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
A6: [x,y] in the InternalRel of RelStr(# f,iP #) and
A7: [y,x] in the InternalRel of RelStr(# f,iP #) ; :: thesis: x = y
consider i, j being Nat, r, s being Real such that
A8: x = [i,r] and
A9: y = [j,s] and
A10: ( i < j & r < s ) by A6, A3;
consider j1, i1 being Nat, s1, r1 being Real such that
A11: y = [j1,s1] and
A12: x = [i1,r1] and
A13: ( j1 < i1 & s1 < r1 ) by A7, A3;
( i = i1 & j = j1 ) by A8, A9, A11, A12, XTUPLE_0:1;
hence x = y by A10, A13; :: thesis: verum

end;

RelStr(# f,iP #) is transitive

proof

let x, y, z be object ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: 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
A14: x in the carrier of RelStr(# f,iP #) and
y in the carrier of RelStr(# f,iP #) and
A15: z in the carrier of RelStr(# f,iP #) and
A16: [x,y] in the InternalRel of RelStr(# f,iP #) and
A17: [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 such that
A18: x = [ix,rx] and
A19: y = [jy,sy] and
A20: ( ix < jy & rx < sy ) by A16, A3;
consider iy, jz being Nat, ry, sz being Real such that
A21: y = [iy,ry] and
A22: z = [jz,sz] and
A23: ( iy < jz & ry < sz ) by A17, A3;
( jy = iy & sy = ry ) by A19, A21, XTUPLE_0:1;
then ( ix < jz & rx < sz ) by A20, A23, XXREAL_0:2;
hence [x,z] in the InternalRel of RelStr(# f,iP #) by A18, A22, A14, A15, A3; :: thesis: verum

end;

then reconsider P = RelStr(# f,iP #) as finite transitive antisymmetric RelStr by A5;
A24: 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 A24, A1, Th55;

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
A25: 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 object ; :: 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 object such that
A26: [x,y] in g by XTUPLE_0:def 12;
x in dom f by A26, XTUPLE_0:def 12;
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 A25; :: thesis: ( g is increasing or g is decreasing )
g is increasing

proof

let e1, e2 be ExtReal; :: according to VALUED_0:def 13 :: thesis: ( not e1 in dom g or not e2 in dom g or e2 <= e1 or not g . e2 <= g . e1 )
assume that
A27: e1 in dom g and
A28: e2 in dom g and
A29: e1 < e2 ; :: thesis: not g . e2 <= g . e1
A30: [e1,(g . e1)] in g by A27, FUNCT_1:1;
A31: [e2,(g . e2)] in g by A28, FUNCT_1:1;
then reconsider p1 = [e1,(g . e1)], p2 = [e2,(g . e2)] as Element of P by A30;
A32: p1 <> p2 by A29, XTUPLE_0:1;

per cases ( p1 <= p2 or p2 <= p1 ) by A30, A31, A32, Th6;

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

then [p1,p2] in iP ;
then consider i, j being Nat, r, s being Real such that
A33: p1 = [i,r] and
A34: p2 = [j,s] and
A35: ( i < j & r < s ) by A3;
( j = e2 & s = g . e2 ) by A34, XTUPLE_0:1;
hence g . e1 < g . e2 by A35, A33, XTUPLE_0:1; :: thesis: verum

end;

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

then [p2,p1] in iP ;
then consider i, j being Nat, r, s being Real such that
A36: p2 = [i,r] and
A37: p1 = [j,s] and
A38: ( i < j & r < s ) by A3;
( i = e2 & j = e1 ) by A36, A37, XTUPLE_0:1;
hence g . e1 < g . e2 by A29, A38; :: 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
A39: card A >= n + 1 ;
set g = A;
reconsider g = A as Subset of f ;
reconsider g = g as Function ;
A40: dom g c= Seg (len f)

proof

let x be object ; :: 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 object such that
A41: [x,y] in g by XTUPLE_0:def 12;
x in dom f by A41, XTUPLE_0:def 12;
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 A39; :: thesis: ( g is increasing or g is decreasing )
g is decreasing

proof

let e1, e2 be ExtReal; :: according to VALUED_0:def 14 :: thesis: ( not e1 in dom g or not e2 in dom g or e2 <= e1 or not g . e1 <= g . e2 )
assume that
A42: e1 in dom g and
A43: e2 in dom g and
A44: e1 < e2 ; :: thesis: not g . e1 <= g . e2
A45: [e1,(g . e1)] in g by A42, FUNCT_1:1;
A46: [e2,(g . e2)] in g by A43, FUNCT_1:1;
then reconsider p1 = [e1,(g . e1)], p2 = [e2,(g . e2)] as Element of P by A45;
A47: p1 <> p2 by A44, XTUPLE_0:1;
( g . e1 = f . e1 & g . e2 = f . e2 ) by A42, A43, GRFUNC_1:2;
then A48: g . e1 <> g . e2 by A4, A40, A42, A43, A44, A2;
reconsider i = e1, j = e2 as Nat by A42, A43;
reconsider r = g . e1, s = g . e2 as Real ;
A49: ( p1 = [i,r] & p2 = [j,s] ) ;

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

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

then [p1,p2] in iP by A45, A3, A44, A49;
then p1 <= p2 ;
hence g . e1 > g . e2 by A45, A46, A47, Def2; :: 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;