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 that
A1: A is_an_arc_of p,q and
A2: a < b and
A3: b <> 1 ; :: thesis:
reconsider B = A as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
consider F being non empty Subset of I[01], s being Function of (I[01] | F),((TOP-REAL n) | B) such that
A4: F = [.a,b.] and
A5: s is being_homeomorphism and
A6: s . a = p and
A7: s . b = q by A1, A2, Th40;
A8: dom s = [#] (I[01] | F) by A5, TOPS_2:def 5
.= F by PRE_TOPC:def 5 ;
then A9: a in dom s by A2, A4, XXREAL_1:1;
reconsider E = ].a,b.] as non empty Subset of I(01) by A2, A3, Th33;
set X = E;
A10: I(01) | E is SubSpace of I[01] by TSEP_1:7;
set sX = s | E;
A11: ( s is continuous & s is one-to-one ) by A5, TOPS_2:def 5;
A12: s " is continuous by A5, TOPS_2:def 5;
A13: the carrier of ((TOP-REAL n) | A) = A by PRE_TOPC:8;
then reconsider Ap = A \ {p} as Subset of ((TOP-REAL n) | A) by XBOOLE_1:36;
the carrier of ((TOP-REAL n) | (A \ {p})) = A \ {p} by PRE_TOPC:8;
then the carrier of ((TOP-REAL n) | (A \ {p})) c= the carrier of ((TOP-REAL n) | A) by A13, XBOOLE_1:36;
then A14: (TOP-REAL n) | (A \ {p}) is SubSpace of (TOP-REAL n) | A by TSEP_1:4;
A15: E c= F by A4, XXREAL_1:23;
then reconsider X9 = E as Subset of (I[01] | F) by PRE_TOPC:8;
A16: (I[01] | F) | X9 is SubSpace of I[01] by TSEP_1:7;
the carrier of (I(01) | E) = E by PRE_TOPC:8;
then the carrier of (I(01) | E) c= the carrier of (I[01] | F) by A15, PRE_TOPC:8;
then A17: I(01) | E is SubSpace of I[01] | F by A10, TSEP_1:4;
A18: ((TOP-REAL n) | A) | Ap = (TOP-REAL n) | (A \ {p}) by PRE_TOPC:7, XBOOLE_1:36;
A19: dom (s | E) = E by A4, A8, RELAT_1:62, XXREAL_1:23
.= [#] (I(01) | E) by PRE_TOPC:def 5 ;
A20: rng s = [#] ((TOP-REAL n) | A) by A5, TOPS_2:def 5;
then A21: rng s = A by PRE_TOPC:def 5;
E = F \ {a} by A2, A4, XXREAL_1:134;
then A22: s .: E = (s .: F) \ (Im (s,a)) by A11, FUNCT_1:64
.= (s .: F) \ {(s . a)} by A9, FUNCT_1:59
.= (rng s) \ {p} by A6, A8, RELAT_1:113
.= [#] ((TOP-REAL n) | (A \ {p})) by A21, PRE_TOPC:def 5 ;
then A23: [#] ((TOP-REAL n) | (A \ {p})) = rng (s | E) by RELAT_1:115;
rng (s | E) = the carrier of ((TOP-REAL n) | (A \ {p})) by A22, RELAT_1:115;
then reconsider sX = s | E as Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) by A19, FUNCT_2:1;
A24: s is onto by A20, FUNCT_2:def 3;
A25: sX is onto by A23, FUNCT_2:def 3;
b in E by A2, XXREAL_1:2;
then A26: sX . b = q by A7, FUNCT_1:49;
the carrier of (I(01) | E) = E by PRE_TOPC:8;
then I(01) | E = (I[01] | F) | X9 by A10, A16, PRE_TOPC:8, TSEP_1:5;
then A27: sX is continuous by A11, A14, Th41;
A28: sX is one-to-one by A11, FUNCT_1:52;
then sX " = sX " by A25, TOPS_2:def 4
.= (s ") | (s .: E) by A11, RFUNCT_2:17
.= (s ") | ([#] ((TOP-REAL n) | (A \ {p}))) by A24, A11, A22, TOPS_2:def 4
.= (s ") | Ap by PRE_TOPC:def 5 ;
then sX " is continuous by A12, A17, A18, Th41;
then sX is being_homeomorphism by A23, A19, A27, A28, TOPS_2:def 5;
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: