let n be Element of NAT ; :: thesis: for D being non empty Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
let D be non empty Subset of (TOP-REAL n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( D is_an_arc_of p1,p2 implies I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic )
assume A1: D is_an_arc_of p1,p2 ; :: thesis: I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
then consider f being Function of I[01] ,((TOP-REAL n) | D) such that
A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by TOPREAL1:def 2;
A3: ( f is continuous & f is one-to-one ) by A2, TOPS_2:def 5;
set fD = f | the carrier of I(01) ;
A4: dom f = the carrier of I[01] by FUNCT_2:def 1;
then A5: dom (f | the carrier of I(01) ) = the carrier of I(01) by BORSUK_1:35, RELAT_1:91;
reconsider K0 = the carrier of I(01) as Subset of I[01] by BORSUK_1:35;
A6: rng f = [#] ((TOP-REAL n) | D) by A2, TOPS_2:def 5
.= D by PRE_TOPC:29 ;
A7: ( 0 in dom f & 1 in dom f ) by A4, BORSUK_1:86;
A8: f .: the carrier of I(01) = (f .: the carrier of I[01] ) \ (f .: {0 ,1}) by A3, Th58, FUNCT_1:123
.= D \ (f .: {0 ,1}) by A4, A6, RELAT_1:146
.= D \ {p1,p2} by A2, A7, FUNCT_1:118 ;
A9: rng (f | the carrier of I(01) ) = f .: the carrier of I(01) by RELAT_1:148;
then A10: rng (f | the carrier of I(01) ) = the carrier of ((TOP-REAL n) | (D \ {p1,p2})) by A8, PRE_TOPC:29;
A11: I(01) = I[01] | K0 by PRE_TOPC:29, TSEP_1:5;
then reconsider fD1 = f | the carrier of I(01) as Function of (I[01] | K0),((TOP-REAL n) | D) by FUNCT_2:38;
A12: fD1 is continuous by A3, TOPMETR:10;
reconsider fD = f | the carrier of I(01) as Function of I(01) ,((TOP-REAL n) | (D \ {p1,p2})) by A5, A10, FUNCT_2:3;
A13: dom fD = [#] I(01) by A4, BORSUK_1:35, RELAT_1:91;
A14: D \ {p1,p2} c= D by XBOOLE_1:36;
reconsider D1 = D \ {p1,p2} as non empty Subset of (TOP-REAL n) by A1, JORDAN6:56;
reconsider D0 = D \ {p1,p2} as Subset of ((TOP-REAL n) | D) by A14, PRE_TOPC:29;
A15: (TOP-REAL n) | D1 = ((TOP-REAL n) | D) | D0 by GOBOARD9:4;
A16: rng fD = [#] ((TOP-REAL n) | (D \ {p1,p2})) by A8, A9, PRE_TOPC:29;
f is one-to-one by A2, TOPS_2:def 5;
then A17: fD is one-to-one by FUNCT_1:84;
A18: fD is continuous by A11, A12, A15, TOPMETR:9;
set g = (f " ) | D1;
A19: f " is continuous by A2, TOPS_2:def 5;
A20: D1 = the carrier of ((TOP-REAL n) | D1) by PRE_TOPC:29;
D1 c= the carrier of ((TOP-REAL n) | D) by A14, PRE_TOPC:29;
then reconsider ff = (f " ) | D1 as Function of ((TOP-REAL n) | D1),I[01] by A20, FUNCT_2:38;
A21: ff is continuous by A15, A19, TOPMETR:10;
rng f = [#] ((TOP-REAL n) | D) by A2, TOPS_2:def 5;
then ( fD " = fD " & f " = f " ) by A3, A10, A17, TOPS_2:def 4;
then fD " is continuous by A3, A8, A11, A21, RFUNCT_2:40, TOPMETR:9;
then fD is being_homeomorphism by A13, A16, A17, A18, TOPS_2:def 5;
hence I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum