reconsider K0 = the carrier of I(01) as Subset of I[01] by BORSUK_1:1;
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 1;
A5: rng f =
[#] ((TOP-REAL n) | D)
by A2, TOPS_2:def 5
.=
D
by PRE_TOPC:8
;
A6:
dom f = the carrier of I[01]
by FUNCT_2:def 1;
then A7:
0 in dom f
by BORSUK_1:43;
A8:
1 in dom f
by A6, BORSUK_1:43;
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 Th30, FUNCT_1:64
.=
D \ (f .: {0,1})
by A6, A5, RELAT_1:113
.=
D \ {p1,p2}
by A3, A4, A7, A8, FUNCT_1:60
;
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:8;
reconsider D1 = D \ {p1,p2} as non empty Subset of (TOP-REAL n) by A1, JORDAN6:43;
A12:
(TOP-REAL n) | D1 = ((TOP-REAL n) | D) | D0
by GOBOARD9:2;
set g = (f ") | D1;
A13:
D1 = the carrier of ((TOP-REAL n) | D1)
by PRE_TOPC:8;
D1 c= the carrier of ((TOP-REAL n) | D)
by A11, PRE_TOPC:8;
then reconsider ff = (f ") | D1 as Function of ((TOP-REAL n) | D1),I[01] by A13, FUNCT_2:32;
f " is continuous
by A2, TOPS_2:def 5;
then A14:
ff is continuous
by A12, TOPMETR:7;
set fD = f | the carrier of I(01);
A15:
I(01) = I[01] | K0
by PRE_TOPC:8, 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:32;
A16:
dom (f | the carrier of I(01)) = the carrier of I(01)
by A6, BORSUK_1:1, RELAT_1:62;
rng f = [#] ((TOP-REAL n) | D)
by A2, TOPS_2:def 5;
then
f is onto
by FUNCT_2:def 3;
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:115;
then A19:
rng (f | the carrier of I(01)) = the carrier of ((TOP-REAL n) | (D \ {p1,p2}))
by A10, PRE_TOPC:8;
then reconsider fD = f | the carrier of I(01) as Function of I(01),((TOP-REAL n) | (D \ {p1,p2})) by A16, FUNCT_2:1;
A20:
dom fD = [#] I(01)
by A6, BORSUK_1:1, RELAT_1:62;
A21:
fD is onto
by A19, FUNCT_2:def 3;
f is one-to-one
by A2, TOPS_2:def 5;
then A22:
fD is one-to-one
by FUNCT_1:52;
then
fD " = fD "
by A21, TOPS_2:def 4;
then A23:
fD " is continuous
by A9, A10, A15, A14, A17, RFUNCT_2:17, TOPMETR:6;
fD1 is continuous
by A9, TOPMETR:7;
then A24:
fD is continuous
by A15, A12, TOPMETR:6;
rng fD = [#] ((TOP-REAL n) | (D \ {p1,p2}))
by A10, A18, PRE_TOPC:8;
then
fD is being_homeomorphism
by A20, A22, A24, A23, TOPS_2:def 5;
hence
I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
by T_0TOPSP:def 1; verum