reconsider a = 0 , b = 1 / 2, c = 1 as Point of I[01] by BORSUK_1:43;
let n be Element of NAT ; for A, B being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q & B is_an_arc_of q,p & A /\ B = {p,q} & p <> q holds
I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
let A, B be Subset of (TOP-REAL n); for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q & B is_an_arc_of q,p & A /\ B = {p,q} & p <> q holds
I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
let p, q be Point of (TOP-REAL n); ( A is_an_arc_of p,q & B is_an_arc_of q,p & A /\ B = {p,q} & p <> q implies I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic )
assume that
A1:
A is_an_arc_of p,q
and
A2:
B is_an_arc_of q,p
and
A3:
A /\ B = {p,q}
and
A4:
p <> q
; I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
consider E2 being non empty Subset of I(01), ty being Function of (I(01) | E2),((TOP-REAL n) | (B \ {p})) such that
A5:
E2 = [.b,c.[
and
A6:
ty is being_homeomorphism
and
A7:
ty . b = q
by A2, Th75;
consider E1 being non empty Subset of I(01), sx being Function of (I(01) | E1),((TOP-REAL n) | (A \ {p})) such that
A8:
E1 = ].a,b.]
and
A9:
sx is being_homeomorphism
and
A10:
sx . b = q
by A1, Th74;
set T1 = I(01) | E1;
set T2 = I(01) | E2;
set T = I(01) ;
set S = (TOP-REAL n) | ((A \ {p}) \/ (B \ {p}));
set U1 = (TOP-REAL n) | (A \ {p});
set U2 = (TOP-REAL n) | (B \ {p});
A11:
not A \ {p} is empty
by A1, Th7;
then reconsider S = (TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) as non empty SubSpace of TOP-REAL n ;
not B \ {p} is empty
by A2, Th7, JORDAN5B:14;
then reconsider U1 = (TOP-REAL n) | (A \ {p}), U2 = (TOP-REAL n) | (B \ {p}) as non empty SubSpace of TOP-REAL n by A11;
A12:
the carrier of S = (A \ {p}) \/ (B \ {p})
by PRE_TOPC:8;
the carrier of U2 = B \ {p}
by PRE_TOPC:8;
then A13:
the carrier of U2 c= the carrier of S
by A12, XBOOLE_1:7;
then reconsider ty9 = ty as Function of (I(01) | E2),S by FUNCT_2:7;
A14:
U2 is SubSpace of S
by A13, TSEP_1:4;
ty is continuous
by A6, TOPS_2:def 5;
then A15:
ty9 is continuous
by A14, PRE_TOPC:26;
reconsider F1 = [#] (I(01) | E1), F2 = [#] (I(01) | E2) as non empty Subset of I(01) by PRE_TOPC:def 5;
A16:
F2 = [.(1 / 2),1.[
by A5, PRE_TOPC:def 5;
the carrier of U1 = A \ {p}
by PRE_TOPC:8;
then A17:
the carrier of U1 c= the carrier of S
by A12, XBOOLE_1:7;
then reconsider sx9 = sx as Function of (I(01) | E1),S by FUNCT_2:7;
A18:
U1 is SubSpace of S
by A17, TSEP_1:4;
A19:
rng ty = [#] ((TOP-REAL n) | (B \ {p}))
by A6, TOPS_2:def 5;
then A20:
rng ty = B \ {p}
by PRE_TOPC:def 5;
B2:
ty is onto
by A19, FUNCT_2:def 3;
A21:
rng sx = [#] ((TOP-REAL n) | (A \ {p}))
by A9, TOPS_2:def 5;
then A22:
rng sx = A \ {p}
by PRE_TOPC:def 5;
then A23: (rng sx9) /\ (rng ty9) =
((A \ {p}) /\ B) \ {p}
by A20, XBOOLE_1:49
.=
((A /\ B) \ {p}) \ {p}
by XBOOLE_1:49
.=
(A /\ B) \ ({p} \/ {p})
by XBOOLE_1:41
.=
{(sx9 . b)}
by A3, A4, A10, ZFMISC_1:17
;
sx is continuous
by A9, TOPS_2:def 5;
then A24:
sx9 is continuous
by A18, PRE_TOPC:26;
A25:
1 / 2 in the carrier of I[01]
by BORSUK_1:43;
then A26:
F2 is closed
by A16, Th73;
A27:
F1 = ].0,(1 / 2).]
by A8, PRE_TOPC:def 5;
then A28: ([#] (I(01) | E1)) \/ ([#] (I(01) | E2)) =
].0,1.[
by A16, XXREAL_1:172
.=
[#] I(01)
by Def1
;
A29:
([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) = {(1 / 2)}
by A27, A16, XXREAL_1:138;
A30:
for d being set st d in ([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) holds
sx . d = ty . d
F1 is closed
by A25, A27, Th72;
then consider F being Function of I(01),S such that
A31:
F = sx9 +* ty
and
A32:
F is continuous
by A24, A15, A26, A28, A30, JGRAPH_2:1;
A33:
[#] U2 = B \ {p}
by PRE_TOPC:def 5;
then A34:
[#] U2 c= (A \ {p}) \/ (B \ {p})
by XBOOLE_1:7;
the carrier of (I(01) | E2) c= the carrier of I(01)
by BORSUK_1:1;
then reconsider g = ty " as Function of U2,I(01) by FUNCT_2:7;
the carrier of (I(01) | E1) c= the carrier of I(01)
by BORSUK_1:1;
then reconsider f = sx " as Function of U1,I(01) by FUNCT_2:7;
A35:
dom ty9 = [#] (I(01) | E2)
by FUNCT_2:def 1;
A36:
[#] U1 = A \ {p}
by PRE_TOPC:def 5;
then
[#] U1 c= (A \ {p}) \/ (B \ {p})
by XBOOLE_1:7;
then reconsider V1 = [#] U1, V2 = [#] U2 as Subset of S by A34, PRE_TOPC:8;
A37:
dom F = [#] I(01)
by FUNCT_2:def 1;
A38:
V2 is closed
proof
reconsider B9 =
B as
Subset of
(TOP-REAL n) ;
A39:
B9 is
closed
by A2, COMPTS_1:7, JORDAN5A:1;
A40:
not
p in {q}
by A4, TARSKI:def 1;
q in B
by A2, TOPREAL1:1;
then A41:
{q} c= B
by ZFMISC_1:31;
A42:
B /\ (A \ {p}) =
(B /\ A) \ {p}
by XBOOLE_1:49
.=
{q}
by A3, A4, ZFMISC_1:17
;
B9 /\ ([#] S) =
B9 /\ ((A \ {p}) \/ (B \ {p}))
by PRE_TOPC:def 5
.=
(B /\ (A \ {p})) \/ (B /\ (B \ {p}))
by XBOOLE_1:23
.=
(B /\ (A \ {p})) \/ (B \ {p})
by XBOOLE_1:28, XBOOLE_1:36
.=
B \ {p}
by A40, A41, A42, XBOOLE_1:12, ZFMISC_1:34
.=
V2
by PRE_TOPC:def 5
;
hence
V2 is
closed
by A39, PRE_TOPC:13;
verum
end;
A43:
V1 is closed
proof
reconsider A9 =
A as
Subset of
(TOP-REAL n) ;
A44:
A9 is
closed
by A1, COMPTS_1:7, JORDAN5A:1;
A45:
not
p in {q}
by A4, TARSKI:def 1;
q in A
by A1, TOPREAL1:1;
then A46:
{q} c= A
by ZFMISC_1:31;
A47:
A /\ (B \ {p}) =
(A /\ B) \ {p}
by XBOOLE_1:49
.=
{q}
by A3, A4, ZFMISC_1:17
;
A9 /\ ([#] S) =
A9 /\ ((A \ {p}) \/ (B \ {p}))
by PRE_TOPC:def 5
.=
(A /\ (A \ {p})) \/ (A /\ (B \ {p}))
by XBOOLE_1:23
.=
(A \ {p}) \/ (A /\ (B \ {p}))
by XBOOLE_1:28, XBOOLE_1:36
.=
A \ {p}
by A45, A46, A47, XBOOLE_1:12, ZFMISC_1:34
.=
V1
by PRE_TOPC:def 5
;
hence
V1 is
closed
by A44, PRE_TOPC:13;
verum
end;
ty " is continuous
by A6, TOPS_2:def 5;
then A48:
g is continuous
by PRE_TOPC:26;
sx " is continuous
by A9, TOPS_2:def 5;
then A49:
f is continuous
by PRE_TOPC:26;
A50:
ty9 is one-to-one
by A6, TOPS_2:def 5;
then A51:
ty " = ty "
by B2, TOPS_2:def 4;
A52:
dom sx9 = [#] (I(01) | E1)
by FUNCT_2:def 1;
then A53:
(dom sx9) /\ (dom ty9) = {b}
by A27, A16, A35, XXREAL_1:138;
sx9 tolerates ty9
then A54: rng F =
(rng sx9) \/ (rng ty9)
by A31, FRECHET:35
.=
[#] S
by A22, A20, PRE_TOPC:def 5
;
B3:
sx is onto
by A21, FUNCT_2:def 3;
A55:
sx9 is one-to-one
by A9, TOPS_2:def 5;
then A56:
sx " = sx "
by B3, TOPS_2:def 4;
A57:
for r being set st r in ([#] U1) /\ ([#] U2) holds
f . r = g . r
proof
let r be
set ;
( r in ([#] U1) /\ ([#] U2) implies f . r = g . r )
b in E2
by A5, XXREAL_1:3;
then A58:
b in dom ty
by A35, PRE_TOPC:def 5;
b in E1
by A8, XXREAL_1:2;
then
b in dom sx
by A52, PRE_TOPC:def 5;
then A59:
f . q = b
by A10, A55, A56, FUNCT_1:34;
assume
r in ([#] U1) /\ ([#] U2)
;
f . r = g . r
then
r = q
by A10, A21, A19, A23, TARSKI:def 1;
hence
f . r = g . r
by A7, A50, A51, A58, A59, FUNCT_1:34;
verum
end;
([#] U1) \/ ([#] U2) = [#] S
by A36, A33, PRE_TOPC:def 5;
then A60:
ex h being Function of S,I(01) st
( h = f +* g & h is continuous )
by A18, A14, A43, A38, A49, A48, A57, JGRAPH_2:1;
VV:
F is onto
by A54, FUNCT_2:def 3;
A61:
F is one-to-one
by A31, A55, A50, A53, A23, Th5;
then
F " = F "
by VV, TOPS_2:def 4;
then
F " = (sx ") +* (ty ")
by A10, A7, A31, A55, A50, A53, A23, A56, A51, Th6;
then
F is being_homeomorphism
by A32, A37, A61, A54, A60, TOPS_2:def 5;
hence
I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
by T_0TOPSP:def 1; verum