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 & 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 (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 & 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 A3, TOPREAL1:def 8;

then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of the carrier 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 = 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 A2, TOPS_1:8;

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 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 & 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 (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 & 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 A3, TOPREAL1:def 8;

then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of the carrier 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 = 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 A2, TOPS_1:8;

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

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

(LSeg (f,i)) /\ Q <> {} by A5, A8, XBOOLE_0:def 4;

then A82: LSeg (f,i) meets Q ;

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def 3;

then A83: R is_an_arc_of f /. i,f /. (i + 1) by A11, TOPREAL1:9;

First_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by A5, A8, XBOOLE_0:def 4;

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;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[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 = First_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: 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 = 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

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

consider hh being Function of (I[01] | Poz),((TOP-REAL 2) | R) such that

A27: hh = F | Poz and

A28: hh is being_homeomorphism by A3, A4, A13, A14, A23, JORDAN5B:8;

A29: hh = F * (id Poz) by A27, RELAT_1:65;

A30: [.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;

Poz = [#] A by A20, TOPMETR:18;

then A31: I[01] | Poz = A by PRE_TOPC:def 5;

hh " is being_homeomorphism by A28, TOPS_2:56;

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 A17, A30, XBOOLE_0:def 4;

then A33: pi1 in dom hh by A27, RELAT_1:61;

then A34: hh . pi1 = f /. (i + 1) by A25, A27, FUNCT_1:47;

the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)

.= P by PRE_TOPC:def 5 ;

then reconsider SEG = LSeg (f,i) as non empty Subset of the carrier of ((TOP-REAL 2) | P) by A5, TOPREAL3:19;

A35: the carrier of (((TOP-REAL 2) | P) | SEG) = [#] (((TOP-REAL 2) | P) | SEG)

.= SEG by PRE_TOPC:def 5 ;

reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ;

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 = 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 A36, TOPS_2:def 5;

reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | P) ;

A43: ((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2;

ppi in [.ppi,pi1.] by A26, RCOMP_1:def 1;

then ppi in (dom F) /\ Poz by A17, A30, XBOOLE_0:def 4;

then A44: ppi in dom hh by A27, RELAT_1:61;

then A45: hh . ppi = f /. i by A24, A27, FUNCT_1:47;

A46: dom hh = [#] (I[01] | Poz) by A28, TOPS_2:def 5;

then A47: dom hh = Poz by PRE_TOPC:def 5;

A48: rng hh = hh .: (dom hh) by A46, RELSET_1:22

.= [#] (((TOP-REAL 2) | P) | SEG) by A23, A35, A27, A47, RELAT_1:129 ;

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 A41, A50, XXREAL_0:2;

then reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace (0,1)) by A40, A41, A49, BORSUK_1:43, TOPMETR:20;

A52: ( F is one-to-one & rng F = [#] ((TOP-REAL 2) | P) ) by A13, TOPS_2:def 5;

set H = (hh ") * g;

A53: rng g = [#] ((TOP-REAL 2) | SE) by A36, TOPS_2:def 5;

set ss = ((hh ") * g) . t;

A54: hh is one-to-one by A28, TOPS_2:def 5;

A55: hh is one-to-one by A28, TOPS_2:def 5;

then A56: dom (hh ") = [#] (((TOP-REAL 2) | P) | SEG) by A43, A48, TOPS_2:49;

then A57: rng ((hh ") * g) = rng (hh ") by A53, RELAT_1:28;

A58: rng (hh ") = [#] (I[01] | Poz) by A43, A55, A48, TOPS_2:49

.= Poz by PRE_TOPC:def 5 ;

then rng ((hh ") * g) = Poz by A53, A56, RELAT_1:28;

then A59: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR:18;

hh is onto by A43, A48, FUNCT_2:def 3;

then A60: hh " = hh " by A55, TOPS_2:def 4;

A61: dom g = [#] I[01] by A36, TOPS_2:def 5

.= the carrier of I[01] ;

then A62: dom ((hh ") * g) = the carrier of (Closed-Interval-TSpace (0,1)) by A43, A53, A56, RELAT_1:27, TOPMETR:20;

A63: t in dom g by A61, A49, A51, BORSUK_1:43;

then g . t in [#] ((TOP-REAL 2) | SE) by A53, FUNCT_1:def 3;

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 A23, FUNCT_1:def 6;

A68: F is one-to-one by A52;

then A69: (F ") . (g . t) in Poz by A65, A66, A67, FUNCT_1:32;

F is onto by A52, FUNCT_2:def 3;

then A70: F " = F " by A52, TOPS_2:def 4;

x = (F ") . (g . t) by A68, A65, A67, FUNCT_1:32;

then (F ") . (g . t) in Poz by A66, A70;

then A71: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17;

g . t in the carrier of ((TOP-REAL 2) | P) by A64;

then A72: g . t in dom (F ") by A52, TOPS_2:49;

t in dom ((hh ") * g) by A43, A53, A63, A56, RELAT_1:27;

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 A63, FUNCT_1:13

.= (F * ((F ") * ((id Poz) "))) . (g . t) by A68, A29, A60, FUNCT_1:44

.= (((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 A72, FUNCT_1:13

.= F . ((id Poz) . ((F ") . (g . t))) by A71, FUNCT_1:13

.= F . ((F ") . (g . t)) by A69, A70, FUNCT_1:17

.= g . t by A52, A64, FUNCT_1:35 ;

1 in dom g by A61, BORSUK_1:43;

then A74: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by A38, FUNCT_1:13

.= pi1 by A54, A33, A34, A60, FUNCT_1:32 ;

0 in dom g by A61, BORSUK_1:43;

then A75: ((hh ") * g) . 0 = (hh ") . (f /. i) by A37, FUNCT_1:13

.= ppi by A54, A44, A45, A60, FUNCT_1:32 ;

dom ((hh ") * g) = dom g by A43, A53, A56, RELAT_1:27;

then ((hh ") * g) . t in Poz by A58, A63, A57, 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

A76: ss9 = ((hh ") * g) . t and

A77: ppi <= ss9 and

ss9 <= pi1 ;

reconsider H = (hh ") * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by A62, A59, FUNCT_2:2;

A78: ss9 = H . w2 by A76;

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 A79: s21 in Poz by A15, A68, FUNCT_1:def 4;

then hh . s21 = g . s2 by A16, A39, A27, FUNCT_1:49;

then s21 = (hh ") . (g . s2) by A55, A47, A79, FUNCT_1:32;

then A80: s21 = (hh ") . (g . s2) by A60;

s2 in dom g by A40, A41, A61, BORSUK_1:43;

then s21 = H . w1 by A80, FUNCT_1:13;

then ss9 < s21 by A20, A50, A75, A74, A42, A32, A31, A78, JORDAN5A:15, TOPMETR:20;

hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A21, A76, A77, A73, Def1; :: 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;

consider hh being Function of (I[01] | Poz),((TOP-REAL 2) | R) such that

A27: hh = F | Poz and

A28: hh is being_homeomorphism by A3, A4, A13, A14, A23, JORDAN5B:8;

A29: hh = F * (id Poz) by A27, RELAT_1:65;

A30: [.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;

Poz = [#] A by A20, TOPMETR:18;

then A31: I[01] | Poz = A by PRE_TOPC:def 5;

hh " is being_homeomorphism by A28, TOPS_2:56;

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 A17, A30, XBOOLE_0:def 4;

then A33: pi1 in dom hh by A27, RELAT_1:61;

then A34: hh . pi1 = f /. (i + 1) by A25, A27, FUNCT_1:47;

the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)

.= P by PRE_TOPC:def 5 ;

then reconsider SEG = LSeg (f,i) as non empty Subset of the carrier of ((TOP-REAL 2) | P) by A5, TOPREAL3:19;

A35: the carrier of (((TOP-REAL 2) | P) | SEG) = [#] (((TOP-REAL 2) | P) | SEG)

.= SEG by PRE_TOPC:def 5 ;

reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ;

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 = 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 A36, TOPS_2:def 5;

reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | P) ;

A43: ((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2;

ppi in [.ppi,pi1.] by A26, RCOMP_1:def 1;

then ppi in (dom F) /\ Poz by A17, A30, XBOOLE_0:def 4;

then A44: ppi in dom hh by A27, RELAT_1:61;

then A45: hh . ppi = f /. i by A24, A27, FUNCT_1:47;

A46: dom hh = [#] (I[01] | Poz) by A28, TOPS_2:def 5;

then A47: dom hh = Poz by PRE_TOPC:def 5;

A48: rng hh = hh .: (dom hh) by A46, RELSET_1:22

.= [#] (((TOP-REAL 2) | P) | SEG) by A23, A35, A27, A47, RELAT_1:129 ;

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 A41, A50, XXREAL_0:2;

then reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace (0,1)) by A40, A41, A49, BORSUK_1:43, TOPMETR:20;

A52: ( F is one-to-one & rng F = [#] ((TOP-REAL 2) | P) ) by A13, TOPS_2:def 5;

set H = (hh ") * g;

A53: rng g = [#] ((TOP-REAL 2) | SE) by A36, TOPS_2:def 5;

set ss = ((hh ") * g) . t;

A54: hh is one-to-one by A28, TOPS_2:def 5;

A55: hh is one-to-one by A28, TOPS_2:def 5;

then A56: dom (hh ") = [#] (((TOP-REAL 2) | P) | SEG) by A43, A48, TOPS_2:49;

then A57: rng ((hh ") * g) = rng (hh ") by A53, RELAT_1:28;

A58: rng (hh ") = [#] (I[01] | Poz) by A43, A55, A48, TOPS_2:49

.= Poz by PRE_TOPC:def 5 ;

then rng ((hh ") * g) = Poz by A53, A56, RELAT_1:28;

then A59: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR:18;

hh is onto by A43, A48, FUNCT_2:def 3;

then A60: hh " = hh " by A55, TOPS_2:def 4;

A61: dom g = [#] I[01] by A36, TOPS_2:def 5

.= the carrier of I[01] ;

then A62: dom ((hh ") * g) = the carrier of (Closed-Interval-TSpace (0,1)) by A43, A53, A56, RELAT_1:27, TOPMETR:20;

A63: t in dom g by A61, A49, A51, BORSUK_1:43;

then g . t in [#] ((TOP-REAL 2) | SE) by A53, FUNCT_1:def 3;

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 A23, FUNCT_1:def 6;

A68: F is one-to-one by A52;

then A69: (F ") . (g . t) in Poz by A65, A66, A67, FUNCT_1:32;

F is onto by A52, FUNCT_2:def 3;

then A70: F " = F " by A52, TOPS_2:def 4;

x = (F ") . (g . t) by A68, A65, A67, FUNCT_1:32;

then (F ") . (g . t) in Poz by A66, A70;

then A71: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17;

g . t in the carrier of ((TOP-REAL 2) | P) by A64;

then A72: g . t in dom (F ") by A52, TOPS_2:49;

t in dom ((hh ") * g) by A43, A53, A63, A56, RELAT_1:27;

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 A63, FUNCT_1:13

.= (F * ((F ") * ((id Poz) "))) . (g . t) by A68, A29, A60, FUNCT_1:44

.= (((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 A72, FUNCT_1:13

.= F . ((id Poz) . ((F ") . (g . t))) by A71, FUNCT_1:13

.= F . ((F ") . (g . t)) by A69, A70, FUNCT_1:17

.= g . t by A52, A64, FUNCT_1:35 ;

1 in dom g by A61, BORSUK_1:43;

then A74: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by A38, FUNCT_1:13

.= pi1 by A54, A33, A34, A60, FUNCT_1:32 ;

0 in dom g by A61, BORSUK_1:43;

then A75: ((hh ") * g) . 0 = (hh ") . (f /. i) by A37, FUNCT_1:13

.= ppi by A54, A44, A45, A60, FUNCT_1:32 ;

dom ((hh ") * g) = dom g by A43, A53, A56, RELAT_1:27;

then ((hh ") * g) . t in Poz by A58, A63, A57, 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

A76: ss9 = ((hh ") * g) . t and

A77: ppi <= ss9 and

ss9 <= pi1 ;

reconsider H = (hh ") * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by A62, A59, FUNCT_2:2;

A78: ss9 = H . w2 by A76;

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 A79: s21 in Poz by A15, A68, FUNCT_1:def 4;

then hh . s21 = g . s2 by A16, A39, A27, FUNCT_1:49;

then s21 = (hh ") . (g . s2) by A55, A47, A79, FUNCT_1:32;

then A80: s21 = (hh ") . (g . s2) by A60;

s2 in dom g by A40, A41, A61, BORSUK_1:43;

then s21 = H . w1 by A80, FUNCT_1:13;

then ss9 < s21 by A20, A50, A75, A74, A42, A32, A31, A78, JORDAN5A:15, TOPMETR:20;

hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A21, A76, A77, A73, Def1; :: thesis: verum

(LSeg (f,i)) /\ Q <> {} by A5, A8, XBOOLE_0:def 4;

then A82: LSeg (f,i) meets Q ;

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def 3;

then A83: R is_an_arc_of f /. i,f /. (i + 1) by A11, TOPREAL1:9;

First_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by A5, A8, XBOOLE_0:def 4;

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