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