let f be FinSequence of (TOP-REAL 2); :: thesis:
let Q be Subset of (TOP-REAL 2); :: thesis:
let i be Element of NAT ; :: thesis:
A1: L~ f is closed by SPPOL_1:49;
assume A2: ( 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 ) ; :: thesis:
then A3: f is one-to-one by TOPREAL1:def 10;
len f >= 2 by A2, TOPREAL1:def 10;
then reconsider P = L~ f, R = LSeg f,i as non empty Subset of the carrier of (TOP-REAL 2) by A2, TOPREAL1:29;
A4: ( L~ f meets Q & (L~ f) /\ Q is closed & P is_an_arc_of f /. 1,f /. (len f) ) by A1, A2, TOPREAL1:31, TOPS_1:35;
then First_Point P,(f /. 1),(f /. (len f)),Q in (L~ f) /\ Q by Def1;
then A5: ( First_Point P,(f /. 1),(f /. (len f)),Q in L~ f & First_Point P,(f /. 1),(f /. (len f)),Q in Q ) by XBOOLE_0:def 4;
set FPO = First_Point R,(f /. i),(f /. (i + 1)),Q;
set FPG = First_Point P,(f /. 1),(f /. (len f)),Q;
A6: ( i in dom f & i + 1 in dom f ) by A2, GOBOARD2:3;
A7: f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis:
then i = i + 1 by A3, A6, PARTFUN2:17;
hence contradiction ; :: thesis:

end;

First_Point P,(f /. 1),(f /. (len f)),Q = First_Point R,(f /. i),(f /. (i + 1)),Q

proof

A8: LSeg f,i is closed by SPPOL_1:40;
A9: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A2, TOPREAL1:def 5;
(LSeg f,i) /\ Q <> {} by A2, A5, XBOOLE_0:def 4;
then A10: ( LSeg f,i meets Q & (LSeg f,i) /\ Q is closed & R is_an_arc_of f /. i,f /. (i + 1) ) by A2, A7, A8, A9, TOPREAL1:15, TOPS_1:35, XBOOLE_0:def 7;
( First_Point P,(f /. 1),(f /. (len f)),Q in (L~ f) /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & 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 ) ) by A4, Def1;
then A11: 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
A12: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) ) by A4, TOPREAL1:def 2;
A13: dom F = [#] I[01] by A12, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
rng F = [#] ((TOP-REAL 2) | P) by A12, TOPS_2:def 5
.= L~ f by PRE_TOPC:def 10 ;
then consider s21 being set such that
A14: ( s21 in dom F & F . s21 = First_Point P,(f /. 1),(f /. (len f)),Q ) by A11, FUNCT_1:def 5;
reconsider s21 = s21 as Real by A13, A14;
A15: ( 0 <= s21 & s21 <= 1 ) by A14, BORSUK_1:86;
A16: First_Point P,(f /. 1),(f /. (len f)),Q in (LSeg f,i) /\ Q by A2, A5, XBOOLE_0:def 4;
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

let g be Function of I[01] ,((TOP-REAL 2) | R); :: thesis:
let s2 be Real; :: thesis:
assume A17: ( 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 ) ; :: thesis:
consider ppi, pi1 being Real such that
A18: ( ppi < pi1 & 0 <= ppi & ppi <= 1 & 0 <= pi1 & pi1 <= 1 & LSeg f,i = F .: [.ppi,pi1.] & F . ppi = f /. i & F . pi1 = f /. (i + 1) ) by A2, A12, JORDAN5B:7;
A19: ( ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } & pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } ) by A18;
then A20: ( ppi in [.ppi,pi1.] & pi1 in [.ppi,pi1.] ) by RCOMP_1:def 1;
A21: [.ppi,pi1.] c= [.0 ,1.] by A18, XXREAL_1:34;
reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A18, A19, BORSUK_1:83, RCOMP_1:def 1, XXREAL_1:34;
the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def 10 ;
then reconsider SEG = LSeg f,i as non empty Subset of the carrier of ((TOP-REAL 2) | P) by A2, TOPREAL3:26;
A22: the carrier of (((TOP-REAL 2) | P) | SEG) = [#] (((TOP-REAL 2) | P) | SEG)
.= SEG by PRE_TOPC:def 10 ;
reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ;
reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | P) ;
A23: ((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE by GOBOARD9:4;
consider hh being Function of (I[01] | Poz),((TOP-REAL 2) | R) such that
A24: ( hh = F | Poz & hh is being_homeomorphism ) by A2, A12, A18, JORDAN5B:8;
A25: ( F is continuous & F is one-to-one ) by A12, TOPS_2:def 5;
A26: hh is one-to-one by A24, TOPS_2:def 5;
A27: hh is one-to-one by A24, TOPS_2:def 5;
A28: dom hh = [#] (I[01] | Poz) by A24, TOPS_2:def 5;
then A29: dom hh = Poz by PRE_TOPC:def 10;
A30: rng hh = hh .: (dom hh) by A28, FUNCT_2:45
.= [#] (((TOP-REAL 2) | P) | SEG) by A18, A22, A24, A29, RELAT_1:162 ;
reconsider A = Closed-Interval-TSpace ppi,pi1 as strict SubSpace of I[01] by A18, TOPMETR:27, TREAL_1:6;
A31: Poz = [#] A by A18, TOPMETR:25;
A32: rng g = [#] ((TOP-REAL 2) | SE) by A17, TOPS_2:def 5;
A33: rng (hh " ) = [#] (I[01] | Poz) by A23, A26, A30, TOPS_2:62
.= Poz by PRE_TOPC:def 10 ;
set H = (hh " ) * g;
A34: hh = F * (id Poz) by A24, RELAT_1:94;
A35: dom g = [#] I[01] by A17, TOPS_2:def 5
.= the carrier of I[01] ;
let t be Real; :: thesis:
assume A36: ( 0 <= t & t < s2 ) ; :: thesis:
then A37: t < 1 by A17, XXREAL_0:2;
then A38: t in dom g by A35, A36, BORSUK_1:86;
( ppi in (dom F) /\ Poz & pi1 in (dom F) /\ Poz ) by A13, A20, A21, XBOOLE_0:def 4;
then A39: ( ppi in dom hh & pi1 in dom hh ) by A24, RELAT_1:90;
then A40: ( hh . ppi = f /. i & hh . pi1 = f /. (i + 1) ) by A18, A24, FUNCT_1:70;
0 in dom g by A35, BORSUK_1:86;
then A41: ((hh " ) * g) . 0 = (hh " ) . (f /. i) by A17, FUNCT_1:23
.= (hh " ) . (f /. i) by A23, A27, A30, TOPS_2:def 4
.= ppi by A27, A39, A40, FUNCT_1:54 ;
1 in dom g by A35, BORSUK_1:86;
then A42: ((hh " ) * g) . 1 = (hh " ) . (f /. (i + 1)) by A17, FUNCT_1:23
.= (hh " ) . (f /. (i + 1)) by A23, A27, A30, TOPS_2:def 4
.= pi1 by A27, A39, A40, FUNCT_1:54 ;
set ss = ((hh " ) * g) . t;
A43: dom (hh " ) = [#] (((TOP-REAL 2) | P) | SEG) by A23, A26, A30, TOPS_2:62;
then A44: ( dom ((hh " ) * g) = dom g & rng ((hh " ) * g) = rng (hh " ) ) by A23, A32, RELAT_1:46, RELAT_1:47;
A45: rng ((hh " ) * g) = Poz by A32, A33, A43, RELAT_1:47;
((hh " ) * g) . t in Poz by A33, A38, A44, FUNCT_1:def 5;
then ((hh " ) * g) . t in { l where l is Real : ( ppi <= l & l <= pi1 ) } by RCOMP_1:def 1;
then consider ss' being Real such that
A46: ( ss' = ((hh " ) * g) . t & ppi <= ss' & ss' <= pi1 ) ;
A47: F is one-to-one by A12, TOPS_2:def 5;
A48: rng F = [#] ((TOP-REAL 2) | P) by A12, TOPS_2:def 5;
g . t in [#] ((TOP-REAL 2) | SE) by A32, A38, FUNCT_1:def 5;
then A49: g . t in SEG by PRE_TOPC:def 10;
then A50: g . t in the carrier of ((TOP-REAL 2) | P) ;
A51: t in dom ((hh " ) * g) by A23, A32, A38, A43, RELAT_1:46;
A52: g . t in dom (F " ) by A47, A48, A50, TOPS_2:62;
consider x being set such that
A53: ( x in dom F & x in Poz & g . t = F . x ) by A18, A49, FUNCT_1:def 12;
x = (F " ) . (g . t) by A25, A53, FUNCT_1:54;
then A54: (F " ) . (g . t) in Poz by A47, A48, A53, TOPS_2:def 4;
A55: (F " ) . (g . t) in Poz by A25, A53, FUNCT_1:54;
A56: (F " ) . (g . t) in dom (id Poz) by A54, FUNCT_1:34;
consider z being set such that
A57: ( z in dom F & z in Poz & F . s21 = F . z ) by A2, A14, A18, FUNCT_1:def 12;
A58: s21 in Poz by A14, A25, A57, FUNCT_1:def 8;
A59: s2 in dom g by A17, A35, BORSUK_1:86;
hh . s21 = g . s2 by A14, A17, A24, A58, FUNCT_1:72;
then s21 = (hh " ) . (g . s2) by A26, A29, A58, FUNCT_1:54;
then A60: s21 = (hh " ) . (g . s2) by A23, A26, A30, TOPS_2:def 4;
A61: dom ((hh " ) * g) = the carrier of (Closed-Interval-TSpace 0 ,1) by A23, A32, A35, A43, RELAT_1:46, TOPMETR:27;
rng ((hh " ) * g) c= the carrier of (Closed-Interval-TSpace ppi,pi1) by A18, A45, TOPMETR:25;
then reconsider H = (hh " ) * g as Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace ppi,pi1) by A61, FUNCT_2:4;
reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace 0 ,1) by A17, A36, A37, BORSUK_1:86, TOPMETR:27;
A62: ( g is continuous & g is one-to-one ) by A17, TOPS_2:def 5;
hh " is being_homeomorphism by A24, TOPS_2:70;
then A63: ( hh " is continuous & hh " is one-to-one ) by TOPS_2:def 5;
I[01] | Poz = A by A31, PRE_TOPC:def 10;
then A64: ( H is continuous & H is one-to-one ) by A62, A63, TOPMETR:27;
( s21 = H . w1 & ss' = H . w2 & t < s2 & ppi < pi1 ) by A18, A36, A46, A59, A60, FUNCT_1:23;
then A65: ss' < s21 by A41, A42, A64, JORDAN5A:16;
F . (((hh " ) * g) . t) = (((hh " ) * g) * F) . t by A51, FUNCT_1:23
.= (g * ((hh " ) * F)) . t by RELAT_1:55
.= (F * (hh " )) . (g . t) by A38, FUNCT_1:23
.= (F * (hh " )) . (g . t) by A23, A26, A30, TOPS_2:def 4
.= (F * ((F " ) * ((id Poz) " ))) . (g . t) by A25, A34, FUNCT_1:66
.= (((F " ) * ((id Poz) " )) * F) . (g . t) by A47, A48, TOPS_2:def 4
.= ((F " ) * (((id Poz) " ) * F)) . (g . t) by RELAT_1:55
.= ((F " ) * (F * (id Poz))) . (g . t) by FUNCT_1:67
.= (F * (id Poz)) . ((F " ) . (g . t)) by A52, FUNCT_1:23
.= F . ((id Poz) . ((F " ) . (g . t))) by A56, FUNCT_1:23
.= F . ((id Poz) . ((F " ) . (g . t))) by A47, A48, TOPS_2:def 4
.= F . ((F " ) . (g . t)) by A55, FUNCT_1:34
.= g . t by A47, A48, A49, FUNCT_1:57 ;
hence not g . t in Q by A4, A12, A14, A15, A18, A46, A65, Def1; :: thesis:

end;

hence First_Point P,(f /. 1),(f /. (len f)),Q = First_Point R,(f /. i),(f /. (i + 1)),Q by A10, A16, Def1; :: thesis:

end;

hence First_Point (L~ f),(f /. 1),(f /. (len f)),Q = First_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q ; :: thesis: