let n be Element of NAT ; for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
let A be Subset of (TOP-REAL n); for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
let p, q be Point of (TOP-REAL n); for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
let a, b be Point of I[01]; ( A is_an_arc_of p,q & a < b & a <> 0 implies ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p ) )
assume that
A1:
A is_an_arc_of p,q
and
A2:
a < b
and
A3:
a <> 0
; ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
reconsider B = A as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
consider F being non empty Subset of I[01], s being Function of (I[01] | F),((TOP-REAL n) | B) such that
A4:
F = [.a,b.]
and
A5:
s is being_homeomorphism
and
A6:
s . a = p
and
A7:
s . b = q
by A1, A2, Th40;
A8: dom s =
[#] (I[01] | F)
by A5, TOPS_2:def 5
.=
F
by PRE_TOPC:def 5
;
then A9:
b in dom s
by A2, A4, XXREAL_1:1;
reconsider E = [.a,b.[ as non empty Subset of I(01) by A2, A3, Th34;
set X = E;
A10:
I(01) | E is SubSpace of I[01]
by TSEP_1:7;
set sX = s | E;
A11:
( s is continuous & s is one-to-one )
by A5, TOPS_2:def 5;
A12:
s " is continuous
by A5, TOPS_2:def 5;
A13:
the carrier of ((TOP-REAL n) | A) = A
by PRE_TOPC:8;
then reconsider Ap = A \ {q} as Subset of ((TOP-REAL n) | A) by XBOOLE_1:36;
the carrier of ((TOP-REAL n) | (A \ {q})) = A \ {q}
by PRE_TOPC:8;
then
the carrier of ((TOP-REAL n) | (A \ {q})) c= the carrier of ((TOP-REAL n) | A)
by A13, XBOOLE_1:36;
then A14:
(TOP-REAL n) | (A \ {q}) is SubSpace of (TOP-REAL n) | A
by TSEP_1:4;
A15:
E c= F
by A4, XXREAL_1:24;
then reconsider X9 = E as Subset of (I[01] | F) by PRE_TOPC:8;
A16:
(I[01] | F) | X9 is SubSpace of I[01]
by TSEP_1:7;
the carrier of (I(01) | E) = E
by PRE_TOPC:8;
then
the carrier of (I(01) | E) c= the carrier of (I[01] | F)
by A15, PRE_TOPC:8;
then A17:
I(01) | E is SubSpace of I[01] | F
by A10, TSEP_1:4;
A18:
((TOP-REAL n) | A) | Ap = (TOP-REAL n) | (A \ {q})
by PRE_TOPC:7, XBOOLE_1:36;
A19: dom (s | E) =
E
by A4, A8, RELAT_1:62, XXREAL_1:24
.=
[#] (I(01) | E)
by PRE_TOPC:def 5
;
A20:
rng s = [#] ((TOP-REAL n) | A)
by A5, TOPS_2:def 5;
then A21:
rng s = A
by PRE_TOPC:def 5;
E = F \ {b}
by A2, A4, XXREAL_1:135;
then A22: s .: E =
(s .: F) \ (Im (s,b))
by A11, FUNCT_1:64
.=
(s .: F) \ {(s . b)}
by A9, FUNCT_1:59
.=
(rng s) \ {q}
by A7, A8, RELAT_1:113
.=
[#] ((TOP-REAL n) | (A \ {q}))
by A21, PRE_TOPC:def 5
;
then A23:
[#] ((TOP-REAL n) | (A \ {q})) = rng (s | E)
by RELAT_1:115;
rng (s | E) = the carrier of ((TOP-REAL n) | (A \ {q}))
by A22, RELAT_1:115;
then reconsider sX = s | E as Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) by A19, FUNCT_2:1;
A24:
sX is onto
by A23, FUNCT_2:def 3;
A25:
s is onto
by A20, FUNCT_2:def 3;
a in E
by A2, XXREAL_1:3;
then A26:
sX . a = p
by A6, FUNCT_1:49;
the carrier of (I(01) | E) = E
by PRE_TOPC:8;
then
I(01) | E = (I[01] | F) | X9
by A10, A16, PRE_TOPC:8, TSEP_1:5;
then A27:
sX is continuous
by A11, A14, Th41;
A28:
sX is one-to-one
by A11, FUNCT_1:52;
then sX " =
sX "
by A24, TOPS_2:def 4
.=
(s ") | (s .: E)
by A11, RFUNCT_2:17
.=
(s ") | ([#] ((TOP-REAL n) | (A \ {q})))
by A25, A11, A22, TOPS_2:def 4
.=
(s ") | Ap
by PRE_TOPC:def 5
;
then
sX " is continuous
by A12, A17, A18, Th41;
then
sX is being_homeomorphism
by A23, A19, A27, A28, TOPS_2:def 5;
hence
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
by A26; verum