let f be FinSequence of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2)

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 (TOP-REAL 2); :: 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 A1, TOPREAL1:def 8;

then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) 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 A2, TOPREAL1:21;

then A4: f /. (i + 1) in P by SPPOL_2:17;

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 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds

s1 <= s2

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

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 (TOP-REAL 2); :: 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 A1, TOPREAL1:def 8;

then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) 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 A2, TOPREAL1:21;

then A4: f /. (i + 1) in P by SPPOL_2:17;

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 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds

s1 <= s2

proof

q in P
by A3, SPPOL_2:17;
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 = 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[01] by A6, TOPS_2:def 5

.= the carrier of I[01] ;

then A13: s2 in dom g by A11, BORSUK_1:43;

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 A1, A2, A6, A7, JORDAN5B:7;

A18: r2 in dom g by A14, A15, A12, BORSUK_1:43;

consider r39 being object such that

A19: r39 in dom g and

A20: r39 in [.r1,r2.] and

A21: g . r39 = q by A3, A16, FUNCT_1:def 6;

r39 in { l where l is Real : ( r1 <= l & l <= r2 ) } by A20, RCOMP_1:def 1;

then consider r3 being Real such that

A22: r3 = r39 and

r1 <= r3 and

A23: r3 <= r2 ;

A24: g is one-to-one by A6, TOPS_2:def 5;

s1 in dom g by A9, A12, BORSUK_1:43;

then s1 = r3 by A8, A19, A21, A22, A24, FUNCT_1:def 4;

hence s1 <= s2 by A10, A17, A23, A18, A13, A24, FUNCT_1:def 4; :: thesis: verum

end;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[01] by A6, TOPS_2:def 5

.= the carrier of I[01] ;

then A13: s2 in dom g by A11, BORSUK_1:43;

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 A1, A2, A6, A7, JORDAN5B:7;

A18: r2 in dom g by A14, A15, A12, BORSUK_1:43;

consider r39 being object such that

A19: r39 in dom g and

A20: r39 in [.r1,r2.] and

A21: g . r39 = q by A3, A16, FUNCT_1:def 6;

r39 in { l where l is Real : ( r1 <= l & l <= r2 ) } by A20, RCOMP_1:def 1;

then consider r3 being Real such that

A22: r3 = r39 and

r1 <= r3 and

A23: r3 <= r2 ;

A24: g is one-to-one by A6, TOPS_2:def 5;

s1 in dom g by A9, A12, BORSUK_1:43;

then s1 = r3 by A8, A19, A21, A22, A24, FUNCT_1:def 4;

hence s1 <= s2 by A10, A17, A23, A18, A13, A24, FUNCT_1:def 4; :: thesis: verum

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