let f be FinSequence of (TOP-REAL 2); :: thesis: for Q being Subset of (TOP-REAL 2)
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 (TOP-REAL 2); :: 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 A3, TOPREAL1:def 8;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5, TOPREAL1:23;
A6: P is_an_arc_of f /. 1,f /. (len f) by A3, TOPREAL1:25;
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 A2, TOPS_1:8;
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 A4, SEQ_4:134;
A10: ( f is one-to-one & i in dom f ) by A3, A4, SEQ_4:134, TOPREAL1:def 8;
A11: f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis: contradiction
then i = i + 1 by A10, A9, PARTFUN2:10;
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[01],((TOP-REAL 2) | P) such that
A13: F is being_homeomorphism and
A14: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) by A6, TOPREAL1:def 1;
rng F = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5
.= 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 A12, FUNCT_1:def 3;
A17: dom F = [#] I[01] by A13, TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40 ;
then reconsider s21 = s21 as Real by A15;
A18: ( 0 <= s21 & s21 <= 1 ) by A15, BORSUK_1:43;
A19: for g being Function of I[01],((TOP-REAL 2) | 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 A3, A4, A13, A14, JORDAN5B:7;
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[01] by A21, A22, BORSUK_1:40, RCOMP_1:def 1, XXREAL_1:34;
A27: [.ppi,pi1.] c= [.0,1.] by A21, A22, XXREAL_1:34;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I[01] by A20, A21, A22, TOPMETR:20, TREAL_1:3;
A28: Poz = [#] A by A20, TOPMETR:18;
then A29: I[01] | Poz = A by PRE_TOPC:def 5;
Closed-Interval-TSpace (ppi,pi1) is compact by A20, HEINE:4;
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 A20, TOPMETR:18;
then Poz is compact by A28, COMPTS_1:2;
then A30: I[01] | Poz is compact by COMPTS_1:3;
reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A6;
let g be Function of I[01],((TOP-REAL 2) | 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 ((TOP-REAL 2) | Lf) = [#] ((TOP-REAL 2) | Lf)
.= Lf by PRE_TOPC:def 5 ;
then reconsider SEG = LSeg (f,i) as non empty Subset of ((TOP-REAL 2) | Lf) by A5, TOPREAL3:19;
reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ;
A37: rng g = [#] ((TOP-REAL 2) | SE) by A31, TOPS_2:def 5;
set gg = F | Poz;
A38: the carrier of (I[01] | Poz) = [#] (I[01] | Poz)
.= Poz by PRE_TOPC:def 5 ;
then reconsider gg = F | Poz as Function of (I[01] | Poz),((TOP-REAL 2) | 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 A42, RELAT_1:61;
then j in dom F by XBOOLE_0:def 4;
then F . j in LSeg (f,i) by A23, A38, A42, FUNCT_1:def 6;
hence ii in SEG by A38, A42, A43, FUNCT_1:49; :: thesis: verum

end;

A44: the carrier of (((TOP-REAL 2) | Lf) | SEG) = [#] (((TOP-REAL 2) | Lf) | SEG)
.= SEG by PRE_TOPC:def 5 ;
reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | Lf) ;
reconsider hh9 = gg as Function of (I[01] | Poz),(((TOP-REAL 2) | Lf) | SEG) by A44, A41, FUNCT_2:6;
reconsider hh = hh9 as Function of (I[01] | Poz),((TOP-REAL 2) | SE) by GOBOARD9:2;
A45: dom hh = [#] (I[01] | Poz) by FUNCT_2:def 1;
then A46: dom hh = Poz by PRE_TOPC:def 5;
A47: rng hh = hh .: (dom hh) by A45, RELSET_1:22
.= [#] (((TOP-REAL 2) | Lf) | SEG) by A23, A44, A46, RELAT_1:129 ;
A48: F is one-to-one by A13, TOPS_2:def 5;
then A49: hh is one-to-one by FUNCT_1:52;
set H = (hh ") * g;
A50: ((TOP-REAL 2) | Lf) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2;
A51: hh9 is one-to-one by A48, FUNCT_1:52;
then A52: dom (hh ") = [#] (((TOP-REAL 2) | Lf) | SEG) by A50, A47, TOPS_2:49;
then A53: rng ((hh ") * g) = rng (hh ") by A37, RELAT_1:28;
A54: dom g = [#] I[01] by A31, TOPS_2:def 5
.= the carrier of I[01] ;
then A55: dom ((hh ") * g) = the carrier of (Closed-Interval-TSpace (0,1)) by A50, A37, A52, RELAT_1:27, TOPMETR:20;
A56: t in dom g by A35, A54, A39, A40, BORSUK_1:43;
then g . t in [#] ((TOP-REAL 2) | SE) by A37, FUNCT_1:def 3;
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 A23, FUNCT_1:def 6;
hh is onto by A50, A47, FUNCT_2:def 3;
then A61: hh " = hh " by A51, TOPS_2:def 4;
A62: (F ") . (g . t) in Poz by A48, A58, A59, A60, FUNCT_1:32;
ex z being object st
( z in dom F & z in Poz & F . s21 = F . z ) by A5, A16, A23, FUNCT_1:def 6;
then A63: s21 in Poz by A15, A48, FUNCT_1:def 4;
then hh . s21 = g . s2 by A16, A34, FUNCT_1:49;
then s21 = (hh ") . (g . s2) by A51, A46, A63, FUNCT_1:32;
then A64: s21 = (hh ") . (g . s2) by A61;
A65: ( g is continuous & g is one-to-one ) by A31, TOPS_2:def 5;
A66: (TOP-REAL 2) | SE is T_2 by TOPMETR:2;
reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace (0,1)) by A35, A36, A39, A40, BORSUK_1:43, TOPMETR:20;
A67: hh = F * (id Poz) by RELAT_1:65;
set ss = ((hh ") * g) . t;
A68: ( F is one-to-one & rng F = [#] ((TOP-REAL 2) | P) ) by A13, TOPS_2:def 5;
A69: rng (hh ") = [#] (I[01] | Poz) by A50, A51, A47, TOPS_2:49
.= Poz by PRE_TOPC:def 5 ;
then rng ((hh ") * g) = Poz by A37, A52, RELAT_1:28;
then A70: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR:18;
dom ((hh ") * g) = dom g by A50, A37, A52, RELAT_1:27;
then ((hh ") * g) . t in Poz by A69, A56, A53, FUNCT_1:def 3;
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 A68, FUNCT_2:def 3;
then A73: F " = F " by A68, TOPS_2:def 4;
A74: 1 >= ss9 by A22, A72, XXREAL_0:2;
x = (F ") . (g . t) by A48, A58, A60, FUNCT_1:32;
then (F ") . (g . t) in Poz by A59, A73;
then A75: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17;
g . t in the carrier of ((TOP-REAL 2) | Lf) by A57;
then A76: g . t in dom (F ") by A68, TOPS_2:49;
t in dom ((hh ") * g) by A50, A37, A56, A52, RELAT_1:27;
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 A56, FUNCT_1:13
.= (F * (hh ")) . (g . t) by A61
.= (F * ((F ") * ((id Poz) "))) . (g . t) by A48, A67, FUNCT_1:44
.= (((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 A76, FUNCT_1:13
.= F . ((id Poz) . ((F ") . (g . t))) by A75, FUNCT_1:13
.= F . ((id Poz) . ((F ") . (g . t))) by A73
.= F . ((F ") . (g . t)) by A62, FUNCT_1:17
.= g . t by A68, A57, FUNCT_1:35 ;
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 A17, A27, XBOOLE_0:def 4;
then A78: pi1 in dom hh by RELAT_1:61;
then A79: hh . pi1 = f /. (i + 1) by A25, FUNCT_1:47;
F is continuous by A13, TOPS_2:def 5;
then gg is continuous by TOPMETR:7;
then hh is being_homeomorphism by A50, A51, A47, A30, A66, COMPTS_1:17, TOPMETR:6;
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 A26, RCOMP_1:def 1;
then ppi in (dom F) /\ Poz by A17, A27, XBOOLE_0:def 4;
then A81: ppi in dom hh by RELAT_1:61;
then A82: hh . ppi = f /. i by A24, FUNCT_1:47;
1 in dom g by A54, BORSUK_1:43;
then A83: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by A33, FUNCT_1:13
.= pi1 by A49, A78, A79, A61, FUNCT_1:32 ;
0 in dom g by A54, BORSUK_1:43;
then A84: ((hh ") * g) . 0 = (hh ") . (f /. i) by A32, FUNCT_1:13
.= ppi by A49, A81, A82, A61, FUNCT_1:32 ;
reconsider H = (hh ") * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by A55, A70, FUNCT_2:2;
s2 in dom g by A35, A36, A54, BORSUK_1:43;
then A85: s21 = H . w1 by A64, FUNCT_1:13;
ss9 = H . w2 by A71;
then ss9 > s21 by A20, A40, A84, A83, A65, A80, A29, A85, JORDAN5A:15, TOPMETR:20;
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 A2, TOPS_1:8;
(LSeg (f,i)) /\ Q <> {} by A5, A8, XBOOLE_0:def 4;
then A87: LSeg (f,i) meets Q ;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def 3;
then A88: R is_an_arc_of f /. i,f /. (i + 1) by A11, TOPREAL1:9;
Last_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by A5, A8, XBOOLE_0:def 4;
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