let f be FinSequence of (); :: thesis: for q being Point of ()
for i being Nat st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)

let q be Point of (); :: thesis: for i being Nat st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE q,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 & q in LSeg (f,i) implies LE q,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 ) and
A3: q in LSeg (f,i) ; :: thesis: LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)
len f >= 2 by ;
then reconsider P = L~ f as non empty Subset of () by TOPREAL1:23;
set p1 = f /. 1;
set p2 = f /. (len f);
set q1 = f /. (i + 1);
f /. (i + 1) in LSeg (f,i) by ;
then A4: f /. (i + 1) in P by SPPOL_2:17;
A5: for g being Function of I,(() | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds
s1 <= s2
proof
let g be Function of I,(() | P); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 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 = q & 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 = q 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 by
.= the carrier of I ;
then A13: s2 in dom g by ;
consider r1, r2 being Real such that
A14: ( r1 < r2 & 0 <= r1 ) and
r1 <= 1 and
0 <= r2 and
A15: r2 <= 1 and
A16: LSeg (f,i) = g .: [.r1,r2.] and
g . r1 = f /. i and
A17: g . r2 = f /. (i + 1) by ;
A18: r2 in dom g by ;
consider r39 being object such that
A19: r39 in dom g and
A20: r39 in [.r1,r2.] and
A21: g . r39 = q by ;
r39 in { l where l is Real : ( r1 <= l & l <= r2 ) } by ;
then consider r3 being Real such that
A22: r3 = r39 and
r1 <= r3 and
A23: r3 <= r2 ;
A24: g is one-to-one by ;
s1 in dom g by ;
then s1 = r3 by ;
hence s1 <= s2 by ; :: thesis: verum
end;
q in P by ;
hence LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A5; :: thesis: verum