let f be FinSequence of (TOP-REAL 2); :: thesis:
let i be Element of NAT ; :: thesis:
assume A1: ( f is being_S-Seq & 1 <= i & i + 1 <= len f ) ; :: thesis:
set p1 = f /. 1;
set p2 = f /. (len f);
set q1 = f /. i;
set q2 = f /. (i + 1);
A2: len f >= 2 by A1, TOPREAL1:def 10;
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:29;
A3: ( i in dom f & i + 1 in dom f ) by A1, GOBOARD2:3;
then A4: f /. i in P by A2, GOBOARD1:16;
A5: f /. (i + 1) in P by A2, A3, GOBOARD1:16;
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 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds
s1 <= s2

let g be Function of I[01] ,((TOP-REAL 2) | P); :: thesis:
let s1, s2 be Real; :: thesis:
assume A6: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 ) ; :: thesis:
then consider r1, r2 being Real such that
A7: ( r1 < r2 & 0 <= r1 & r1 <= 1 & 0 <= r2 & r2 <= 1 & LSeg f,i = g .: [.r1,r2.] & g . r1 = f /. i & g . r2 = f /. (i + 1) ) by A1, JORDAN5B:7;
dom g = [#] I[01] by A6, TOPS_2:def 5
.= the carrier of I[01] ;
then A8: ( r1 in dom g & s1 in dom g & r2 in dom g & s2 in dom g ) by A6, A7, BORSUK_1:86;
g is one-to-one by A6, TOPS_2:def 5;
then ( s1 = r1 & s2 = r2 ) by A6, A7, A8, FUNCT_1:def 8;
hence s1 <= s2 by A7; :: thesis:

end;

hence LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A5, Def3; :: thesis: