let f be FinSequence of (TOP-REAL 2); :: thesis:
let q1, q2 be Point of (TOP-REAL 2); :: thesis:
set p3 = f /. 1;
set p4 = f /. (len f);
assume that
A1: q1 in L~ f and
A2: q2 in L~ f and
A3: f is being_S-Seq and
A4: q1 <> q2 ; :: thesis:
reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A1;

hereby :: thesis:

assume A5: LE q1,q2, L~ f,f /. 1,f /. (len f) ; :: thesis:
thus for i, j being Nat st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) :: thesis:

proof

let i, j be Nat; :: thesis:
assume that
A6: q1 in LSeg (f,i) and
A7: q2 in LSeg (f,j) and
A8: 1 <= i and
A9: i + 1 <= len f and
A10: ( 1 <= j & j + 1 <= len f ) ; :: thesis:
thus i <= j :: thesis:

proof

assume j < i ; :: thesis:
then j + 1 <= i by NAT_1:13;
then consider m being Nat such that
A11: (j + 1) + m = i by NAT_1:10;
A12: LE q2,f /. (j + 1),P,f /. 1,f /. (len f) by A3, A7, A10, Th26;
reconsider m = m as Nat ;
A13: ( 1 <= j + 1 & j + 1 <= (j + 1) + m ) by NAT_1:11;
i <= i + 1 by NAT_1:11;
then (j + 1) + m <= len f by A9, A11, XXREAL_0:2;
then LE f /. (j + 1),f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A3, A13, Th24;
then A14: LE q2,f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A12, Th13;
LE f /. ((j + 1) + m),q1,P,f /. 1,f /. (len f) by A3, A6, A8, A9, A11, Th25;
then LE q2,q1,P,f /. 1,f /. (len f) by A14, Th13;
hence contradiction by A3, A4, A5, Th12, TOPREAL1:25; :: thesis:

end;

assume A15: i = j ; :: thesis:
A16: f is one-to-one by A3, TOPREAL1:def 8;
set p1 = f /. i;
set p2 = f /. (i + 1);
A17: ( i in dom f & i + 1 in dom f ) by A8, A9, SEQ_4:134;
A18: f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis:
then i = i + 1 by A17, A16, PARTFUN2:10;
hence contradiction ; :: thesis:

end;

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A8, A9, TOPREAL1:def 3;
hence LE q1,q2,f /. i,f /. (i + 1) by A3, A5, A6, A7, A8, A9, A15, A18, Th17, Th29; :: thesis:

end;

consider i being Nat such that
A19: ( 1 <= i & i + 1 <= len f ) and
A20: q1 in LSeg (f,i) by A1, SPPOL_2:13;
consider j being Nat such that
A21: 1 <= j and
A22: j + 1 <= len f and
A23: q2 in LSeg (f,j) by A2, SPPOL_2:13;
assume A24: for i, j being Nat st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ; :: thesis:
then A25: i <= j by A19, A20, A21, A22, A23;

per cases by A25, XXREAL_0:1;

suppose i < j ; :: thesis:

then i + 1 <= j by NAT_1:13;
then consider m being Nat such that
A26: j = (i + 1) + m by NAT_1:10;
reconsider m = m as Nat ;
A27: ( 1 <= i + 1 & i + 1 <= (i + 1) + m ) by NAT_1:11;
A28: LE q1,f /. (i + 1),P,f /. 1,f /. (len f) by A3, A19, A20, Th26;
j <= j + 1 by NAT_1:11;
then (i + 1) + m <= len f by A22, A26, XXREAL_0:2;
then LE f /. (i + 1),f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A3, A27, Th24;
then A29: LE q1,f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A28, Th13;
LE f /. ((i + 1) + m),q2,P,f /. 1,f /. (len f) by A3, A21, A22, A23, A26, Th25;
hence LE q1,q2, L~ f,f /. 1,f /. (len f) by A29, Th13; :: thesis:

end;

suppose A30: i = j ; :: thesis:

reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A20;
set p1 = f /. i;
set p2 = f /. (i + 1);
A31: f is one-to-one by A3, TOPREAL1:def 8;
A32: ( i in dom f & i + 1 in dom f ) by A19, SEQ_4:134;
f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis:
then i = i + 1 by A32, A31, PARTFUN2:10;
hence contradiction ; :: thesis:

end;

then consider H being Function of I[01],((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1))))) such that
A33: for x being Real st x in [.0,1.] holds
H . x = ((1 - x) * (f /. i)) + (x * (f /. (i + 1))) and
A34: H is being_homeomorphism and
H . 0 = f /. i and
H . 1 = f /. (i + 1) by JORDAN5A:3;
A35: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A19, TOPREAL1:def 3;
then reconsider H = H as Function of I[01],((TOP-REAL 2) | Q) ;
A36: LE q1,q2,f /. i,f /. (i + 1) by A24, A19, A20, A23, A30;
( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) )

proof

A37: rng H = [#] ((TOP-REAL 2) | (LSeg (f,i))) by A34, A35, TOPS_2:def 5
.= LSeg (f,i) by PRE_TOPC:def 5 ;
then consider x19 being object such that
A38: x19 in dom H and
A39: H . x19 = q1 by A20, FUNCT_1:def 3;
A40: dom H = [#] I[01] by A34, TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40 ;
then x19 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A38, RCOMP_1:def 1;
then consider x1 being Real such that
A41: x1 = x19 and
0 <= x1 and
A42: x1 <= 1 ;
consider x29 being object such that
A43: x29 in dom H and
A44: H . x29 = q2 by A23, A30, A37, FUNCT_1:def 3;
x29 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A40, A43, RCOMP_1:def 1;
then consider x2 being Real such that
A45: x2 = x29 and
A46: ( 0 <= x2 & x2 <= 1 ) ;
A47: q2 = ((1 - x2) * (f /. i)) + (x2 * (f /. (i + 1))) by A33, A40, A43, A44, A45;
q1 = ((1 - x1) * (f /. i)) + (x1 * (f /. (i + 1))) by A33, A40, A38, A39, A41;
then A48: x1 <= x2 by A36, A42, A46, A47;
0 in { l where l is Real : ( 0 <= l & l <= 1 ) } ;
then A49: 0 in [.0,1.] by RCOMP_1:def 1;
then A50: H . 0 = ((1 - 0) * (f /. i)) + (0 * (f /. (i + 1))) by A33
.= (f /. i) + (0 * (f /. (i + 1))) by RLVECT_1:def 8
.= (f /. i) + (0. (TOP-REAL 2)) by RLVECT_1:10
.= f /. i by RLVECT_1:4 ;
thus ( q1 in P & q2 in P ) by A1, A2; :: thesis:
let F be Function of I[01],((TOP-REAL 2) | P); :: thesis:
let s1, s2 be Real; :: thesis:
assume that
A51: F is being_homeomorphism and
A52: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) and
A53: F . s1 = q1 and
A54: ( 0 <= s1 & s1 <= 1 ) and
A55: F . s2 = q2 and
A56: ( 0 <= s2 & s2 <= 1 ) ; :: thesis:
consider ppi, pi1 being Real such that
A57: ppi < pi1 and
A58: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A59: pi1 <= 1 and
A60: LSeg (f,i) = F .: [.ppi,pi1.] and
A61: F . ppi = f /. i and
A62: F . pi1 = f /. (i + 1) by A3, A19, A51, A52, JORDAN5B:7;
A63: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A57;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A58, A59, BORSUK_1:40, RCOMP_1:def 1, XXREAL_1:34;
consider G being Function of (I[01] | Poz),((TOP-REAL 2) | Q) such that
A64: G = F | Poz and
A65: G is being_homeomorphism by A3, A19, A51, A52, A60, JORDAN5B:8;
A66: dom F = [#] I[01] by A51, TOPS_2:def 5
.= the carrier of I[01] ;
reconsider K1 = Closed-Interval-TSpace (ppi,pi1), K2 = I[01] | Poz as SubSpace of I[01] by A57, A58, A59, TOPMETR:20, TREAL_1:3;
A67: the carrier of K1 = [.ppi,pi1.] by A57, TOPMETR:18
.= [#] (I[01] | Poz) by PRE_TOPC:def 5
.= the carrier of K2 ;
then reconsider E = (G ") * H as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by TOPMETR:20;
A68: G is one-to-one by A65, TOPS_2:def 5;
reconsider X1 = x1, X2 = x2 as Point of (Closed-Interval-TSpace (0,1)) by A40, A38, A41, A43, A45, TOPMETR:18;
A69: G " is being_homeomorphism by A65, TOPS_2:56;
A70: s2 in the carrier of I[01] by A56, BORSUK_1:43;
A71: F is one-to-one by A51, TOPS_2:def 5;
rng G = [#] ((TOP-REAL 2) | (LSeg (f,i))) by A65, TOPS_2:def 5;
then G is onto by FUNCT_2:def 3;
then A72: G " = G " by A68, TOPS_2:def 4;
A73: ex x9 being object st
( x9 in dom F & x9 in [.ppi,pi1.] & q2 = F . x9 ) by A23, A30, A60, FUNCT_1:def 6;
then s2 in Poz by A55, A70, A66, A71, FUNCT_1:def 4;
then A74: G . s2 = q2 by A55, A64, FUNCT_1:49;
dom G = [#] (I[01] | Poz) by A65, TOPS_2:def 5;
then A75: dom G = Poz by PRE_TOPC:def 5;
then s2 in dom G by A55, A70, A66, A71, A73, FUNCT_1:def 4;
then A76: s2 = (G ") . (H . x2) by A44, A45, A68, A72, A74, FUNCT_1:32
.= E . x2 by A43, A45, FUNCT_1:13 ;
then A77: s2 = E . X2 ;
consider x being object such that
A78: x in dom F and
A79: x in [.ppi,pi1.] and
A80: q1 = F . x by A20, A60, FUNCT_1:def 6;
A81: s1 in the carrier of I[01] by A54, BORSUK_1:43;
then x = s1 by A53, A66, A71, A78, A80, FUNCT_1:def 4;
then A82: G . s1 = q1 by A64, A79, A80, FUNCT_1:49;
Closed-Interval-TSpace (ppi,pi1) = I[01] | Poz by A67, TSEP_1:5;
then E is being_homeomorphism by A34, A35, A69, TOPMETR:20, TOPS_2:57;
then A83: ( E is continuous & E is one-to-one ) by TOPS_2:def 5;
1 in { l where l is Real : ( 0 <= l & l <= 1 ) } ;
then A84: 1 in [.0,1.] by RCOMP_1:def 1;
then A85: H . 1 = ((1 - 1) * (f /. i)) + (1 * (f /. (i + 1))) by A33
.= (0. (TOP-REAL 2)) + (1 * (f /. (i + 1))) by RLVECT_1:10
.= (0. (TOP-REAL 2)) + (f /. (i + 1)) by RLVECT_1:def 8
.= f /. (i + 1) by RLVECT_1:4 ;
s1 in dom G by A53, A81, A66, A71, A75, A79, A80, FUNCT_1:def 4;
then A86: s1 = (G ") . (H . x1) by A39, A41, A68, A72, A82, FUNCT_1:32
.= E . x1 by A38, A41, FUNCT_1:13 ;
then A87: s1 = E . X1 ;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A57;
then A88: pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
then G . pi1 = f /. (i + 1) by A62, A64, FUNCT_1:49;
then A89: pi1 = (G ") . (H . 1) by A88, A68, A75, A72, A85, FUNCT_1:32
.= E . 1 by A40, A84, FUNCT_1:13 ;
A90: ppi in [.ppi,pi1.] by A63, RCOMP_1:def 1;
then G . ppi = f /. i by A61, A64, FUNCT_1:49;
then A91: ppi = (G ") . (H . 0) by A90, A68, A75, A72, A50, FUNCT_1:32
.= E . 0 by A40, A49, FUNCT_1:13 ;

per cases by A48, XXREAL_0:1;

suppose x1 = x2 ; :: thesis:

hence s1 <= s2 by A86, A76; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

hence s1 <= s2 by A57, A83, A91, A89, A87, A77, JORDAN5A:15; :: thesis:

end;

hence LE q1,q2, L~ f,f /. 1,f /. (len f) ; :: thesis:

end;