let n be Element of NAT ; :: thesis:
let A be Subset of (TOP-REAL n); :: thesis:
let p, q be Point of (TOP-REAL n); :: thesis:
let a, b be Point of I[01] ; :: thesis:
assume A1: ( A is_an_arc_of p,q & a < b & b <> 1 ) ; :: thesis:
then reconsider B = A as non empty Subset of (TOP-REAL n) by TOPREAL1:4;
consider F being non empty Subset of I[01] , s being Function of (I[01] | F),((TOP-REAL n) | B) such that
A2: ( F = [.a,b.] & s is being_homeomorphism & s . a = p & s . b = q ) by A1, Th68;
reconsider E = ].a,b.] as non empty Subset of I(01) by A1, Th61;
A3: the carrier of (I(01) | E) = E by PRE_TOPC:29;
set X = E;
A4: E = F \ {a} by A1, A2, XXREAL_1:134;
A5: E c= F by A2, XXREAL_1:23;
then reconsider X' = E as Subset of (I[01] | F) by PRE_TOPC:29;
set sX = s | E;
A6: ( s is continuous & s is one-to-one ) by A2, TOPS_2:def 5;
A7: rng s = [#] ((TOP-REAL n) | A) by A2, TOPS_2:def 5;
then A8: rng s = A by PRE_TOPC:def 10;
A9: dom s = [#] (I[01] | F) by A2, TOPS_2:def 5
.= F by PRE_TOPC:def 10 ;
then A10: E c= dom s by A2, XXREAL_1:23;
A11: a in dom s by A1, A2, A9, XXREAL_1:1;
A12: s .: E = (s .: F) \ (Im s,a) by A4, A6, FUNCT_1:123
.= (s .: F) \ {(s . a)} by A11, FUNCT_1:117
.= (rng s) \ {p} by A2, A9, RELAT_1:146
.= [#] ((TOP-REAL n) | (A \ {p})) by A8, PRE_TOPC:def 10 ;
then A13: [#] ((TOP-REAL n) | (A \ {p})) = rng (s | E) by RELAT_1:148;
A14: rng (s | E) = the carrier of ((TOP-REAL n) | (A \ {p})) by A12, RELAT_1:148;
A15: dom (s | E) = E by A10, RELAT_1:91
.= [#] (I(01) | E) by PRE_TOPC:def 10 ;
then reconsider sX = s | E as Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) by A14, FUNCT_2:3;
A16: the carrier of (I(01) | E) = E by PRE_TOPC:29;
A17: I(01) | E is SubSpace of I[01] by TSEP_1:7;
(I[01] | F) | X' is SubSpace of I[01] by TSEP_1:7;
then A18: I(01) | E = (I[01] | F) | X' by A16, A17, PRE_TOPC:29, TSEP_1:5;
A19: the carrier of ((TOP-REAL n) | (A \ {p})) = A \ {p} by PRE_TOPC:29;
A20: the carrier of ((TOP-REAL n) | A) = A by PRE_TOPC:29;
then the carrier of ((TOP-REAL n) | (A \ {p})) c= the carrier of ((TOP-REAL n) | A) by A19, XBOOLE_1:36;
then (TOP-REAL n) | (A \ {p}) is SubSpace of (TOP-REAL n) | A by TSEP_1:4;
then A21: sX is continuous by A6, A18, Th69;
A22: sX is one-to-one by A6, FUNCT_1:84;
A23: s " is continuous by A2, TOPS_2:def 5;
the carrier of (I(01) | E) c= the carrier of (I[01] | F) by A3, A5, PRE_TOPC:29;
then A24: I(01) | E is SubSpace of I[01] | F by A17, TSEP_1:4;
reconsider Ap = A \ {p} as Subset of ((TOP-REAL n) | A) by A20, XBOOLE_1:36;
A25: ((TOP-REAL n) | A) | Ap = (TOP-REAL n) | (A \ {p}) by PRE_TOPC:28, XBOOLE_1:36;
sX " = sX " by A13, A22, TOPS_2:def 4
.= (s " ) | (s .: E) by A6, RFUNCT_2:40
.= (s " ) | ([#] ((TOP-REAL n) | (A \ {p}))) by A6, A7, A12, TOPS_2:def 4
.= (s " ) | Ap by PRE_TOPC:def 10 ;
then sX " is continuous by A23, A24, A25, Th69;
then A26: sX is being_homeomorphism by A13, A15, A21, A22, TOPS_2:def 5;
b in E by A1, XXREAL_1:2;
then sX . b = q by A2, FUNCT_1:72;
hence ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is being_homeomorphism & f . b = q ) by A26; :: thesis: