let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st f is being_S-Seq & 1 <= i & i + 1 <= len f holds
LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)
let i be Nat; :: thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f implies LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: ( 1 <= i & i + 1 <= len f ) ; :: thesis: LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)
set p1 = f /. 1;
set p2 = f /. (len f);
set q1 = f /. i;
set q2 = f /. (i + 1);
A3: len f >= 2 by A1, TOPREAL1:def 8;
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;
i + 1 in dom f by A2, SEQ_4:134;
then A4: f /. (i + 1) in P by A3, GOBOARD1:1;
A5: 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

proof

let g be Function of I[01],((TOP-REAL 2) | P); :: thesis: 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 s1, s2 be Real; :: thesis: ( 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 implies s1 <= s2 )
assume that
A6: g is being_homeomorphism and
A7: ( g . 0 = f /. 1 & g . 1 = f /. (len f) ) and
A8: g . s1 = f /. i and
A9: ( 0 <= s1 & s1 <= 1 ) and
A10: g . s2 = f /. (i + 1) and
A11: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2
A12: dom g = [#] I[01] by A6, TOPS_2:def 5
.= the carrier of I[01] ;
then A13: s1 in dom g by A9, BORSUK_1:43;
A14: s2 in dom g by A11, A12, BORSUK_1:43;
A15: g is one-to-one by A6, TOPS_2:def 5;
consider r1, r2 being Real such that
A16: r1 < r2 and
A17: 0 <= r1 and
A18: r1 <= 1 and
0 <= r2 and
A19: r2 <= 1 and
LSeg (f,i) = g .: [.r1,r2.] and
A20: g . r1 = f /. i and
A21: g . r2 = f /. (i + 1) by A1, A2, A6, A7, JORDAN5B:7;
A22: r2 in dom g by A16, A17, A19, A12, BORSUK_1:43;
r1 in dom g by A17, A18, A12, BORSUK_1:43;
then s1 = r1 by A8, A20, A13, A15, FUNCT_1:def 4;
hence s1 <= s2 by A10, A16, A21, A22, A14, A15, FUNCT_1:def 4; :: thesis: verum

end;

i in dom f by A2, SEQ_4:134;
then f /. i in P by A3, GOBOARD1:1;
hence LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A5; :: thesis: verum