let f be FinSequence of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg f,i holds
LE f /. i,q, L~ f,f /. 1,f /. (len f)
let q be Point of (TOP-REAL 2); :: thesis: for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg f,i holds
LE f /. i,q, L~ f,f /. 1,f /. (len f)
let i be Element of NAT ; :: thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg f,i implies LE f /. i,q, L~ f,f /. 1,f /. (len f) )
assume A1: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg f,i ) ; :: thesis: LE f /. i,q, L~ f,f /. 1,f /. (len f)
then A2: 2 <= len f by TOPREAL1:def 10;
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:29;
set p1 = f /. 1;
set p2 = f /. (len f);
set q1 = f /. i;
i in dom f by A1, GOBOARD2:3;
then A3: f /. i in P by A2, GOBOARD1:16;
A4: q in P by A1, SPPOL_2:17;
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 = q & 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 = q & 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 = q & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume A5: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2
then consider r1, r2 being Real such that
A6: ( 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;
consider r3' being set such that
A7: ( r3' in dom g & r3' in [.r1,r2.] & g . r3' = q ) by A1, A6, FUNCT_1:def 12;
r3' in { l where l is Real : ( r1 <= l & l <= r2 ) } by A7, RCOMP_1:def 1;
then consider r3 being Real such that
A8: ( r3 = r3' & r1 <= r3 & r3 <= r2 ) ;
dom g = [#] I[01] by A5, TOPS_2:def 5
.= the carrier of I[01] ;
then A9: ( r1 in dom g & s1 in dom g & r2 in dom g & s2 in dom g ) by A5, A6, BORSUK_1:86;
A10: g is one-to-one by A5, TOPS_2:def 5;
then s2 = r3 by A5, A7, A8, A9, FUNCT_1:def 8;
hence s1 <= s2 by A5, A6, A8, A9, A10, FUNCT_1:def 8; :: thesis: verum

end;

hence LE f /. i,q, L~ f,f /. 1,f /. (len f) by A3, A4, Def3; :: thesis: verum