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 & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_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 & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_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 & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) implies Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_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: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) ; :: thesis: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_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 () by ;
A6: P is_an_arc_of f /. 1,f /. (len f) by ;
set FPO = Last_Point (R,(f /. i),(f /. (i + 1)),Q);
set FPG = Last_Point (P,(f /. 1),(f /. (len f)),Q);
A7: (L~ f) /\ Q is closed by ;
then Last_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A6, Def2;
then A8: Last_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;
Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q)
proof
Last_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A7, A6, Def2;
then A12: Last_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 = Last_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: ( 0 <= s21 & 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 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= 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 ;
A27: [.ppi,pi1.] c= [.0,1.] by ;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I by ;
A28: Poz = [#] A by ;
then A29: I | Poz = A by PRE_TOPC:def 5;
Closed-Interval-TSpace (ppi,pi1) is compact by ;
then [#] (Closed-Interval-TSpace (ppi,pi1)) is compact by COMPTS_1:1;
then for P being Subset of A st P = Poz holds
P is compact by ;
then Poz is compact by ;
then A30: I | Poz is compact by COMPTS_1:3;
reconsider Lf = L~ f as non empty Subset of () by A6;
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 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= 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 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds
not g . t in Q )

assume that
A31: g is being_homeomorphism and
A32: g . 0 = f /. i and
A33: g . 1 = f /. (i + 1) and
A34: g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) and
A35: 0 <= s2 and
A36: s2 <= 1 ; :: thesis: for t being Real st 1 >= t & t > s2 holds
not g . t in Q

the carrier of (() | Lf) = [#] (() | Lf)
.= Lf by PRE_TOPC:def 5 ;
then reconsider SEG = LSeg (f,i) as non empty Subset of (() | Lf) by ;
reconsider SE = SEG as non empty Subset of () ;
A37: rng g = [#] (() | SE) by ;
set gg = F | Poz;
A38: the carrier of (I | Poz) = [#] (I | Poz)
.= Poz by PRE_TOPC:def 5 ;
then reconsider gg = F | Poz as Function of (I | Poz),(() | P) by FUNCT_2:32;
let t be Real; :: thesis: ( 1 >= t & t > s2 implies not g . t in Q )
assume that
A39: 1 >= t and
A40: t > s2 ; :: thesis: not g . t in Q
A41: rng gg c= SEG
proof
let ii be object ; :: according to TARSKI:def 3 :: thesis: ( not ii in rng gg or ii in SEG )
assume ii in rng gg ; :: thesis: ii in SEG
then consider j being object such that
A42: j in dom gg and
A43: ii = gg . j by FUNCT_1:def 3;
j in (dom F) /\ Poz by ;
then j in dom F by XBOOLE_0:def 4;
then F . j in LSeg (f,i) by ;
hence ii in SEG by ; :: thesis: verum
end;
A44: the carrier of ((() | Lf) | SEG) = [#] ((() | Lf) | SEG)
.= SEG by PRE_TOPC:def 5 ;
reconsider SEG = SEG as non empty Subset of (() | Lf) ;
reconsider hh9 = gg as Function of (I | Poz),((() | Lf) | SEG) by ;
reconsider hh = hh9 as Function of (I | Poz),(() | SE) by GOBOARD9:2;
A45: dom hh = [#] (I | Poz) by FUNCT_2:def 1;
then A46: dom hh = Poz by PRE_TOPC:def 5;
A47: rng hh = hh .: (dom hh) by
.= [#] ((() | Lf) | SEG) by ;
A48: F is one-to-one by ;
then A49: hh is one-to-one by FUNCT_1:52;
set H = (hh ") * g;
A50: ((TOP-REAL 2) | Lf) | SEG = () | SE by GOBOARD9:2;
A51: hh9 is one-to-one by ;
then A52: dom (hh ") = [#] ((() | Lf) | SEG) by ;
then A53: rng ((hh ") * g) = rng (hh ") by ;
A54: dom g = [#] I by
.= the carrier of I ;
then A55: dom ((hh ") * g) = the carrier of () by ;
A56: t in dom g by ;
then g . t in [#] (() | SE) by ;
then A57: g . t in SEG by PRE_TOPC:def 5;
then consider x being object such that
A58: x in dom F and
A59: x in Poz and
A60: g . t = F . x by ;
hh is onto by ;
then A61: hh " = hh " by ;
A62: (F ") . (g . t) in Poz by ;
ex z being object st
( z in dom F & z in Poz & F . s21 = F . z ) by ;
then A63: s21 in Poz by ;
then hh . s21 = g . s2 by ;
then s21 = (hh ") . (g . s2) by ;
then A64: s21 = (hh ") . (g . s2) by A61;
A65: ( g is continuous & g is one-to-one ) by ;
A66: (TOP-REAL 2) | SE is T_2 by TOPMETR:2;
reconsider w1 = s2, w2 = t as Point of () by ;
A67: hh = F * (id Poz) by RELAT_1:65;
set ss = ((hh ") * g) . t;
A68: ( F is one-to-one & rng F = [#] (() | P) ) by ;
A69: rng (hh ") = [#] (I | Poz) by
.= Poz by PRE_TOPC:def 5 ;
then rng ((hh ") * g) = Poz by ;
then A70: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) 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
A71: ss9 = ((hh ") * g) . t and
ppi <= ss9 and
A72: ss9 <= pi1 ;
F is onto by ;
then A73: F " = F " by ;
A74: 1 >= ss9 by ;
x = (F ") . (g . t) by ;
then (F ") . (g . t) in Poz by ;
then A75: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17;
g . t in the carrier of (() | Lf) by A57;
then A76: g . t in dom (F ") by ;
t in dom ((hh ") * g) by ;
then A77: 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 * (hh ")) . (g . t) by A61
.= (F * ((F ") * ((id Poz) "))) . (g . t) by
.= (((F ") * ((id Poz) ")) * F) . (g . t) by A73
.= ((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 . ((id Poz) . ((F ") . (g . t))) by A73
.= F . ((F ") . (g . t)) by
.= g . t by ;
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 A78: pi1 in dom hh by RELAT_1:61;
then A79: hh . pi1 = f /. (i + 1) by ;
F is continuous by ;
then gg is continuous by TOPMETR:7;
then hh is being_homeomorphism by ;
then hh " is being_homeomorphism by TOPS_2:56;
then A80: ( hh " is continuous & hh " is one-to-one ) by TOPS_2:def 5;
ppi in [.ppi,pi1.] by ;
then ppi in (dom F) /\ Poz by ;
then A81: ppi in dom hh by RELAT_1:61;
then A82: hh . ppi = f /. i by ;
1 in dom g by ;
then A83: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by
.= pi1 by ;
0 in dom g by ;
then A84: ((hh ") * g) . 0 = (hh ") . (f /. i) by
.= ppi by ;
reconsider H = (hh ") * g as Function of (),(Closed-Interval-TSpace (ppi,pi1)) by ;
s2 in dom g by ;
then A85: s21 = H . w1 by ;
ss9 = H . w2 by A71;
then ss9 > s21 by ;
hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A71, A74, A77, Def2; :: thesis: verum
end;
A86: (LSeg (f,i)) /\ Q is closed by ;
(LSeg (f,i)) /\ Q <> {} by ;
then A87: LSeg (f,i) meets Q ;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by ;
then A88: R is_an_arc_of f /. i,f /. (i + 1) by ;
Last_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by ;
hence Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) by A87, A86, A88, A19, Def2; :: thesis: verum
end;
hence Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ; :: thesis: verum