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)

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

Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q)
assume
f /. i = f /. (i + 1)
; :: thesis: contradiction

then i = i + 1 by A10, A9, PARTFUN2:10;

hence contradiction ; :: thesis: verum

end;then i = i + 1 by A10, A9, PARTFUN2:10;

hence contradiction ; :: thesis: verum

proof

hence
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
; :: thesis: verum
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

(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;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

A86:
(LSeg (f,i)) /\ Q is closed
by A2, TOPS_1:8;
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

.= 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;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

A44: the carrier of (((TOP-REAL 2) | Lf) | SEG) =
[#] (((TOP-REAL 2) | Lf) | SEG)
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;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

.= 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

(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