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

let Q be Subset of (); :: thesis: for i being Nat st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)

let i be Nat; :: thesis: ( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) )
assume that
A1: L~ f meets Q and
A2: Q is closed and
A3: f is being_S-Seq and
A4: ( 1 <= i & i + 1 <= len f ) and
A5: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) ; :: thesis: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
len f >= 2 by ;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of the carrier of () by ;
A6: P is_an_arc_of f /. 1,f /. (len f) by ;
set FPO = First_Point (R,(f /. i),(f /. (i + 1)),Q);
set FPG = First_Point (P,(f /. 1),(f /. (len f)),Q);
A7: (L~ f) /\ Q is closed by ;
then First_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A6, Def1;
then A8: First_Point (P,(f /. 1),(f /. (len f)),Q) in Q by XBOOLE_0:def 4;
A9: i + 1 in dom f by ;
A10: ( f is one-to-one & i in dom f ) by ;
A11: f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; :: thesis: contradiction
then i = i + 1 by ;
hence contradiction ; :: thesis: verum
end;
First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q)
proof
First_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A7, A6, Def1;
then A12: First_Point (P,(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def 4;
consider F being Function of I,(() | P) such that
A13: F is being_homeomorphism and
A14: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) by ;
rng F = [#] (() | P) by
.= L~ f by PRE_TOPC:def 5 ;
then consider s21 being object such that
A15: s21 in dom F and
A16: F . s21 = First_Point (P,(f /. 1),(f /. (len f)),Q) by ;
A17: dom F = [#] I by
.= [.0,1.] by BORSUK_1:40 ;
then reconsider s21 = s21 as Real by A15;
A18: s21 <= 1 by ;
A19: for g being Function of I,(() | R)
for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
proof
consider ppi, pi1 being Real such that
A20: ppi < pi1 and
A21: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A22: pi1 <= 1 and
A23: LSeg (f,i) = F .: [.ppi,pi1.] and
A24: F . ppi = f /. i and
A25: F . pi1 = f /. (i + 1) by ;
A26: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I by ;
consider hh being Function of (I | Poz),(() | R) such that
A27: hh = F | Poz and
A28: hh is being_homeomorphism by ;
A29: hh = F * (id Poz) by ;
A30: [.ppi,pi1.] c= [.0,1.] by ;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I by ;
Poz = [#] A by ;
then A31: I | Poz = A by PRE_TOPC:def 5;
hh " is being_homeomorphism by ;
then A32: ( hh " is continuous & hh " is one-to-one ) by TOPS_2:def 5;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20;
then pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
then pi1 in (dom F) /\ Poz by ;
then A33: pi1 in dom hh by ;
then A34: hh . pi1 = f /. (i + 1) by ;
the carrier of (() | P) = [#] (() | P)
.= P by PRE_TOPC:def 5 ;
then reconsider SEG = LSeg (f,i) as non empty Subset of the carrier of (() | P) by ;
A35: the carrier of ((() | P) | SEG) = [#] ((() | P) | SEG)
.= SEG by PRE_TOPC:def 5 ;
reconsider SE = SEG as non empty Subset of () ;
let g be Function of I,(() | R); :: thesis: for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q

let s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in Q )

assume that
A36: g is being_homeomorphism and
A37: g . 0 = f /. i and
A38: g . 1 = f /. (i + 1) and
A39: g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) and
A40: 0 <= s2 and
A41: s2 <= 1 ; :: thesis: for t being Real st 0 <= t & t < s2 holds
not g . t in Q

A42: ( g is continuous & g is one-to-one ) by ;
reconsider SEG = SEG as non empty Subset of (() | P) ;
A43: ((TOP-REAL 2) | P) | SEG = () | SE by GOBOARD9:2;
ppi in [.ppi,pi1.] by ;
then ppi in (dom F) /\ Poz by ;
then A44: ppi in dom hh by ;
then A45: hh . ppi = f /. i by ;
A46: dom hh = [#] (I | Poz) by ;
then A47: dom hh = Poz by PRE_TOPC:def 5;
A48: rng hh = hh .: (dom hh) by
.= [#] ((() | P) | SEG) by ;
let t be Real; :: thesis: ( 0 <= t & t < s2 implies not g . t in Q )
assume that
A49: 0 <= t and
A50: t < s2 ; :: thesis: not g . t in Q
A51: t < 1 by ;
then reconsider w1 = s2, w2 = t as Point of () by ;
A52: ( F is one-to-one & rng F = [#] (() | P) ) by ;
set H = (hh ") * g;
A53: rng g = [#] (() | SE) by ;
set ss = ((hh ") * g) . t;
A54: hh is one-to-one by ;
A55: hh is one-to-one by ;
then A56: dom (hh ") = [#] ((() | P) | SEG) by ;
then A57: rng ((hh ") * g) = rng (hh ") by ;
A58: rng (hh ") = [#] (I | Poz) by
.= Poz by PRE_TOPC:def 5 ;
then rng ((hh ") * g) = Poz by ;
then A59: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by ;
hh is onto by ;
then A60: hh " = hh " by ;
A61: dom g = [#] I by
.= the carrier of I ;
then A62: dom ((hh ") * g) = the carrier of () by ;
A63: t in dom g by ;
then g . t in [#] (() | SE) by ;
then A64: g . t in SEG by PRE_TOPC:def 5;
then consider x being object such that
A65: x in dom F and
A66: x in Poz and
A67: g . t = F . x by ;
A68: F is one-to-one by A52;
then A69: (F ") . (g . t) in Poz by ;
F is onto by ;
then A70: F " = F " by ;
x = (F ") . (g . t) by ;
then (F ") . (g . t) in Poz by ;
then A71: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17;
g . t in the carrier of (() | P) by A64;
then A72: g . t in dom (F ") by ;
t in dom ((hh ") * g) by ;
then A73: F . (((hh ") * g) . t) = (((hh ") * g) * F) . t by FUNCT_1:13
.= (g * ((hh ") * F)) . t by RELAT_1:36
.= (F * (hh ")) . (g . t) by
.= (F * ((F ") * ((id Poz) "))) . (g . t) by
.= (((F ") * ((id Poz) ")) * F) . (g . t) by A70
.= ((F ") * (((id Poz) ") * F)) . (g . t) by RELAT_1:36
.= ((F ") * (F * (id Poz))) . (g . t) by FUNCT_1:45
.= (F * (id Poz)) . ((F ") . (g . t)) by
.= F . ((id Poz) . ((F ") . (g . t))) by
.= F . ((F ") . (g . t)) by
.= g . t by ;
1 in dom g by ;
then A74: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by
.= pi1 by ;
0 in dom g by ;
then A75: ((hh ") * g) . 0 = (hh ") . (f /. i) by
.= ppi by ;
dom ((hh ") * g) = dom g by ;
then ((hh ") * g) . t in Poz by ;
then ((hh ") * g) . t in { l where l is Real : ( ppi <= l & l <= pi1 ) } by RCOMP_1:def 1;
then consider ss9 being Real such that
A76: ss9 = ((hh ") * g) . t and
A77: ppi <= ss9 and
ss9 <= pi1 ;
reconsider H = (hh ") * g as Function of (),(Closed-Interval-TSpace (ppi,pi1)) by ;
A78: ss9 = H . w2 by A76;
ex z being object st
( z in dom F & z in Poz & F . s21 = F . z ) by ;
then A79: s21 in Poz by ;
then hh . s21 = g . s2 by ;
then s21 = (hh ") . (g . s2) by ;
then A80: s21 = (hh ") . (g . s2) by A60;
s2 in dom g by ;
then s21 = H . w1 by ;
then ss9 < s21 by ;
hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A21, A76, A77, A73, Def1; :: thesis: verum
end;
A81: (LSeg (f,i)) /\ Q is closed by ;
(LSeg (f,i)) /\ Q <> {} by ;
then A82: LSeg (f,i) meets Q ;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by ;
then A83: R is_an_arc_of f /. i,f /. (i + 1) by ;
First_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by ;
hence First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q) by A82, A81, A83, A19, Def1; :: thesis: verum
end;
hence First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ; :: thesis: verum