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, Th47;
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, Th46;
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, Th3;
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, Th3, 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;
A21:
ty is onto
by A19, FUNCT_2:def 3;
A22:
rng sx = [#] ((TOP-REAL n) | (A \ {p}))
by A9, TOPS_2:def 5;
then A23:
rng sx = A \ {p}
by PRE_TOPC:def 5;
then A24: (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 A25:
sx9 is continuous
by A18, PRE_TOPC:26;
A26:
1 / 2 in the carrier of I[01]
by BORSUK_1:43;
then A27:
F2 is closed
by A16, Th45;
A28:
F1 = ].0,(1 / 2).]
by A8, PRE_TOPC:def 5;
then A29: ([#] (I(01) | E1)) \/ ([#] (I(01) | E2)) =
].0,1.[
by A16, XXREAL_1:172
.=
[#] I(01)
by Def1
;
A30:
([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) = {(1 / 2)}
by A28, A16, XXREAL_1:138;
A31:
for d being object st d in ([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) holds
sx . d = ty . d
F1 is closed
by A26, A28, Th44;
then consider F being Function of I(01),S such that
A32:
F = sx9 +* ty
and
A33:
F is continuous
by A25, A15, A27, A29, A31, JGRAPH_2:1;
A34:
[#] U2 = B \ {p}
by PRE_TOPC:def 5;
then A35:
[#] 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;
A36:
dom ty9 = [#] (I(01) | E2)
by FUNCT_2:def 1;
A37:
[#] 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 A35, PRE_TOPC:8;
A38:
dom F = [#] I(01)
by FUNCT_2:def 1;
A39:
V2 is closed
proof
reconsider B9 =
B as
Subset of
(TOP-REAL n) ;
A40:
B9 is
closed
by A2, COMPTS_1:7, JORDAN5A:1;
A41:
not
p in {q}
by A4, TARSKI:def 1;
q in B
by A2, TOPREAL1:1;
then A42:
{q} c= B
by ZFMISC_1:31;
A43:
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 A41, A42, A43, XBOOLE_1:12, ZFMISC_1:34
.=
V2
by PRE_TOPC:def 5
;
hence
V2 is
closed
by A40, PRE_TOPC:13;
verum
end;
A44:
V1 is closed
proof
reconsider A9 =
A as
Subset of
(TOP-REAL n) ;
A45:
A9 is
closed
by A1, COMPTS_1:7, JORDAN5A:1;
A46:
not
p in {q}
by A4, TARSKI:def 1;
q in A
by A1, TOPREAL1:1;
then A47:
{q} c= A
by ZFMISC_1:31;
A48:
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 A46, A47, A48, XBOOLE_1:12, ZFMISC_1:34
.=
V1
by PRE_TOPC:def 5
;
hence
V1 is
closed
by A45, PRE_TOPC:13;
verum
end;
ty " is continuous
by A6, TOPS_2:def 5;
then A49:
g is continuous
by PRE_TOPC:26;
sx " is continuous
by A9, TOPS_2:def 5;
then A50:
f is continuous
by PRE_TOPC:26;
A51:
ty9 is one-to-one
by A6, TOPS_2:def 5;
then A52:
ty " = ty "
by A21, TOPS_2:def 4;
A53:
dom sx9 = [#] (I(01) | E1)
by FUNCT_2:def 1;
then A54:
(dom sx9) /\ (dom ty9) = {b}
by A28, A16, A36, XXREAL_1:138;
sx9 tolerates ty9
then A55: rng F =
(rng sx9) \/ (rng ty9)
by A32, FRECHET:35
.=
[#] S
by A23, A20, PRE_TOPC:def 5
;
A56:
sx is onto
by A22, FUNCT_2:def 3;
A57:
sx9 is one-to-one
by A9, TOPS_2:def 5;
then A58:
sx " = sx "
by A56, TOPS_2:def 4;
A59:
for r being object st r in ([#] U1) /\ ([#] U2) holds
f . r = g . r
proof
let r be
object ;
( r in ([#] U1) /\ ([#] U2) implies f . r = g . r )
b in E2
by A5, XXREAL_1:3;
then A60:
b in dom ty
by A36, PRE_TOPC:def 5;
b in E1
by A8, XXREAL_1:2;
then
b in dom sx
by A53, PRE_TOPC:def 5;
then A61:
f . q = b
by A10, A57, A58, FUNCT_1:34;
assume
r in ([#] U1) /\ ([#] U2)
;
f . r = g . r
then
r = q
by A10, A22, A19, A24, TARSKI:def 1;
hence
f . r = g . r
by A7, A51, A52, A60, A61, FUNCT_1:34;
verum
end;
([#] U1) \/ ([#] U2) = [#] S
by A37, A34, PRE_TOPC:def 5;
then A62:
ex h being Function of S,I(01) st
( h = f +* g & h is continuous )
by A18, A14, A44, A39, A50, A49, A59, JGRAPH_2:1;
A63:
F is onto
by A55, FUNCT_2:def 3;
A64:
F is one-to-one
by A32, A57, A51, A54, A24, Th1;
then
F " = F "
by A63, TOPS_2:def 4;
then
F " = (sx ") +* (ty ")
by A10, A7, A32, A57, A51, A54, A24, A58, A52, Th2;
then
F is being_homeomorphism
by A33, A38, A64, A55, A62, TOPS_2:def 5;
hence
I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
by T_0TOPSP:def 1; verum