let f be FinSequence of (TOP-REAL 2); 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); 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; ( 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)
; 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
let g be
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 <= s2let s1,
s2 be
Real;
( 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 )
;
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;
verum
end;
q in P
by A3, SPPOL_2:17;
hence
LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)
by A4, A5; verum