let n be Nat; :: thesis: for p being Point of (TOP-REAL n)

for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

let p be Point of (TOP-REAL n); :: thesis: for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

let A, B be Subset of (TOP-REAL n); :: thesis: ( B is closed & p in Int A implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B )

set TRn = TOP-REAL n;

set T = Tunit_circle n;

assume that

A1: B is closed and

A2: p in Int A ; :: thesis: for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

A3: Int A c= A by TOPS_1:16;

A4: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); :: thesis: ( h is being_homeomorphism implies h . p in Int B )

assume A5: h is being_homeomorphism ; :: thesis: h . p in Int B

A6: h " is continuous by A5, TOPS_2:def 5;

A7: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then A8: dom h = A by A5, TOPS_2:def 5;

A9: [#] ((TOP-REAL n) | B) = B by PRE_TOPC:def 5;

then A10: rng h = B by A5, TOPS_2:def 5;

for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

let p be Point of (TOP-REAL n); :: thesis: for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

let A, B be Subset of (TOP-REAL n); :: thesis: ( B is closed & p in Int A implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B )

set TRn = TOP-REAL n;

set T = Tunit_circle n;

assume that

A1: B is closed and

A2: p in Int A ; :: thesis: for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

A3: Int A c= A by TOPS_1:16;

A4: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); :: thesis: ( h is being_homeomorphism implies h . p in Int B )

assume A5: h is being_homeomorphism ; :: thesis: h . p in Int B

A6: h " is continuous by A5, TOPS_2:def 5;

A7: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then A8: dom h = A by A5, TOPS_2:def 5;

A9: [#] ((TOP-REAL n) | B) = B by PRE_TOPC:def 5;

then A10: rng h = B by A5, TOPS_2:def 5;

per cases
( n = 0 or n > 0 )
;

end;

suppose A11:
n > 0
; :: thesis: h . p in Int B

A12:
h . p in rng h
by A2, A3, A8, FUNCT_1:def 3;

then reconsider hp = h . p as Point of (TOP-REAL n) by A10;

ex r being Real st

( r > 0 & ( for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,r) holds

ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ U) <> f ) ) ) )

then hp in B \ (Fr B) by A12, A9, XBOOLE_0:def 5;

hence h . p in Int B by TOPS_1:40; :: thesis: verum

end;then reconsider hp = h . p as Point of (TOP-REAL n) by A10;

ex r being Real st

( r > 0 & ( for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,r) holds

ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ U) <> f ) ) ) )

proof

then
not hp in Fr B
by A1, Th9;
reconsider hP = hp as Point of (Euclid n) by A4, TOPMETR:12;

not p in Fr A by A2, TOPS_1:39, XBOOLE_0:3;

then consider r being Real such that

A14: r > 0 and

A15: for U being open Subset of ((TOP-REAL n) | A) st p in U & U c= Ball (p,r) holds

ex f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st h is continuous holds

h | (A \ U) <> f ) ) by A11, A2, A3, Th8;

reconsider BA = (Ball (p,r)) /\ A as Subset of ((TOP-REAL n) | A) by A7, XBOOLE_1:17;

Ball (p,r) in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

then BA in the topology of ((TOP-REAL n) | A) by A7, PRE_TOPC:def 4;

then reconsider BA = BA as open Subset of ((TOP-REAL n) | A) by PRE_TOPC:def 2;

h .: BA is open by A5, A2, A3, A12, TOPGRP_1:25;

then h .: BA in the topology of ((TOP-REAL n) | B) by PRE_TOPC:def 2;

then consider U being Subset of (TOP-REAL n) such that

A16: U in the topology of (TOP-REAL n) and

A17: h .: BA = U /\ ([#] ((TOP-REAL n) | B)) by PRE_TOPC:def 4;

reconsider U = U as open Subset of (TOP-REAL n) by A16, PRE_TOPC:def 2;

A18: Int U = U by TOPS_1:23;

p is Element of REAL n by EUCLID:22;

then |.(p - p).| = 0 ;

then p in Ball (p,r) by A14;

then p in BA by A2, A3, XBOOLE_0:def 4;

then hp in h .: BA by A7, A8, FUNCT_1:def 6;

then hp in U by A17, XBOOLE_0:def 4;

then consider s being Real such that

A19: s > 0 and

A20: Ball (hP,s) c= U by A18, GOBOARD6:5;

take s ; :: thesis: ( s > 0 & ( for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,s) holds

ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ U) <> f ) ) ) )

thus s > 0 by A19; :: thesis: for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,s) holds

ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ U) <> f ) )

let W be open Subset of ((TOP-REAL n) | B); :: thesis: ( hp in W & W c= Ball (hp,s) implies ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) ) )

assume that

A21: hp in W and

A22: W c= Ball (hp,s) ; :: thesis: ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) )

A23: W /\ B = W by A9, XBOOLE_1:28;

Ball (hp,s) = Ball (hP,s) by TOPREAL9:13;

then W c= U by A22, A20;

then A24: W c= U /\ B by A23, XBOOLE_1:27;

h " (U /\ B) = h " (h .: BA) by A17, PRE_TOPC:def 5

.= BA by FUNCT_1:94, XBOOLE_1:17, A8, A5 ;

then A25: h " W c= BA by A24, RELAT_1:143;

reconsider hW = h " W as open Subset of ((TOP-REAL n) | A) by TOPS_2:43, A5, A9, A12;

A26: BA c= Ball (p,r) by XBOOLE_1:17;

set BW = B \ W;

reconsider bw = B \ W as Subset of ((TOP-REAL n) | B) by XBOOLE_1:36, A9;

A27: [#] ((TOP-REAL n) | (A \ hW)) = A \ hW by PRE_TOPC:def 5;

p in h " W by A8, A2, A3, A21, FUNCT_1:def 7;

then consider F being Function of ((TOP-REAL n) | (A \ hW)),(Tunit_circle n) such that

A28: F is continuous and

A29: for h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st h is continuous holds

h | (A \ hW) <> F by A15, A25, A26, XBOOLE_1:1;

A30: B \ W c= B by XBOOLE_1:36;

then A31: (h ") .: (B \ W) = h " (B \ W) by TOPS_2:55, A9, A10, A5

.= (h " B) \ hW by FUNCT_1:69

.= A \ hW by RELAT_1:134, A8, A10 ;

end;not p in Fr A by A2, TOPS_1:39, XBOOLE_0:3;

then consider r being Real such that

A14: r > 0 and

A15: for U being open Subset of ((TOP-REAL n) | A) st p in U & U c= Ball (p,r) holds

ex f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st h is continuous holds

h | (A \ U) <> f ) ) by A11, A2, A3, Th8;

reconsider BA = (Ball (p,r)) /\ A as Subset of ((TOP-REAL n) | A) by A7, XBOOLE_1:17;

Ball (p,r) in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

then BA in the topology of ((TOP-REAL n) | A) by A7, PRE_TOPC:def 4;

then reconsider BA = BA as open Subset of ((TOP-REAL n) | A) by PRE_TOPC:def 2;

h .: BA is open by A5, A2, A3, A12, TOPGRP_1:25;

then h .: BA in the topology of ((TOP-REAL n) | B) by PRE_TOPC:def 2;

then consider U being Subset of (TOP-REAL n) such that

A16: U in the topology of (TOP-REAL n) and

A17: h .: BA = U /\ ([#] ((TOP-REAL n) | B)) by PRE_TOPC:def 4;

reconsider U = U as open Subset of (TOP-REAL n) by A16, PRE_TOPC:def 2;

A18: Int U = U by TOPS_1:23;

p is Element of REAL n by EUCLID:22;

then |.(p - p).| = 0 ;

then p in Ball (p,r) by A14;

then p in BA by A2, A3, XBOOLE_0:def 4;

then hp in h .: BA by A7, A8, FUNCT_1:def 6;

then hp in U by A17, XBOOLE_0:def 4;

then consider s being Real such that

A19: s > 0 and

A20: Ball (hP,s) c= U by A18, GOBOARD6:5;

take s ; :: thesis: ( s > 0 & ( for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,s) holds

ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ U) <> f ) ) ) )

thus s > 0 by A19; :: thesis: for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,s) holds

ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ U) <> f ) )

let W be open Subset of ((TOP-REAL n) | B); :: thesis: ( hp in W & W c= Ball (hp,s) implies ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) ) )

assume that

A21: hp in W and

A22: W c= Ball (hp,s) ; :: thesis: ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) )

A23: W /\ B = W by A9, XBOOLE_1:28;

Ball (hp,s) = Ball (hP,s) by TOPREAL9:13;

then W c= U by A22, A20;

then A24: W c= U /\ B by A23, XBOOLE_1:27;

h " (U /\ B) = h " (h .: BA) by A17, PRE_TOPC:def 5

.= BA by FUNCT_1:94, XBOOLE_1:17, A8, A5 ;

then A25: h " W c= BA by A24, RELAT_1:143;

reconsider hW = h " W as open Subset of ((TOP-REAL n) | A) by TOPS_2:43, A5, A9, A12;

A26: BA c= Ball (p,r) by XBOOLE_1:17;

set BW = B \ W;

reconsider bw = B \ W as Subset of ((TOP-REAL n) | B) by XBOOLE_1:36, A9;

A27: [#] ((TOP-REAL n) | (A \ hW)) = A \ hW by PRE_TOPC:def 5;

p in h " W by A8, A2, A3, A21, FUNCT_1:def 7;

then consider F being Function of ((TOP-REAL n) | (A \ hW)),(Tunit_circle n) such that

A28: F is continuous and

A29: for h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st h is continuous holds

h | (A \ hW) <> F by A15, A25, A26, XBOOLE_1:1;

A30: B \ W c= B by XBOOLE_1:36;

then A31: (h ") .: (B \ W) = h " (B \ W) by TOPS_2:55, A9, A10, A5

.= (h " B) \ hW by FUNCT_1:69

.= A \ hW by RELAT_1:134, A8, A10 ;

per cases
( A \ hW is empty or not A \ hW is empty )
;

end;

suppose A32:
A \ hW is empty
; :: thesis: ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) )

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) )

reconsider n1 = n - 1 as Element of NAT by NAT_1:20, A11;

set h = the continuous Function of ((TOP-REAL n) | A),(Tunit_circle (n1 + 1));

reconsider H = the continuous Function of ((TOP-REAL n) | A),(Tunit_circle (n1 + 1)) as Function of ((TOP-REAL n) | A),(Tunit_circle n) ;

A33: H | (A \ hW) = {} by A32;

H | (A \ hW) <> F by A29;

hence ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) ) by A33, A32; :: thesis: verum

end;set h = the continuous Function of ((TOP-REAL n) | A),(Tunit_circle (n1 + 1));

reconsider H = the continuous Function of ((TOP-REAL n) | A),(Tunit_circle (n1 + 1)) as Function of ((TOP-REAL n) | A),(Tunit_circle n) ;

A33: H | (A \ hW) = {} by A32;

H | (A \ hW) <> F by A29;

hence ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) ) by A33, A32; :: thesis: verum

suppose A34:
not A \ hW is empty
; :: thesis: ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) )

( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> f ) )

reconsider hbw = (h ") | (B \ W) as Function of (((TOP-REAL n) | B) | bw),(((TOP-REAL n) | A) | ((h ") .: (B \ W))) by A2, A3, A12, JORDAN24:12;

A35: ((TOP-REAL n) | B) | bw = (TOP-REAL n) | (B \ W) by PRE_TOPC:7, XBOOLE_1:36;

A36: ((TOP-REAL n) | A) | ((h ") .: (B \ W)) = (TOP-REAL n) | (A \ hW) by A31, PRE_TOPC:7, A7;

then reconsider HBW = hbw as Function of ((TOP-REAL n) | (B \ W)),((TOP-REAL n) | (A \ hW)) by A35;

reconsider fhW = F * HBW as Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) by A34;

take fhW ; :: thesis: ( fhW is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> fhW ) )

thus fhW is continuous by A34, JORDAN24:13, A6, A2, A3, A12, A36, A35, A28, TOPS_2:46; :: thesis: for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> fhW

let g be Function of ((TOP-REAL n) | B),(Tunit_circle n); :: thesis: ( g is continuous implies g | (B \ W) <> fhW )

assume A37: g is continuous ; :: thesis: g | (B \ W) <> fhW

reconsider gh = g * h as Function of ((TOP-REAL n) | A),(Tunit_circle n) by A12;

A38: gh is continuous by A5, A12, A37, TOPS_2:46;

assume A39: g | (B \ W) = fhW ; :: thesis: contradiction

A40: dom F = A \ hW by FUNCT_2:def 1, A11, A27;

A41: rng (h | (A \ hW)) = h .: (A \ hW) by RELAT_1:115

.= h .: (h " (B \ W)) by TOPS_2:55, A9, A10, A31, A5, A30

.= B \ W by FUNCT_1:77, A10, XBOOLE_1:36 ;

gh | (A \ hW) = g * (h | (A \ hW)) by RELAT_1:83

.= g * ((id (B \ W)) * (h | (A \ hW))) by A41, RELAT_1:53

.= (g * (id (B \ W))) * (h | (A \ hW)) by RELAT_1:36

.= (g | (B \ W)) * (h | (A \ hW)) by RELAT_1:65

.= F * (((h ") | (B \ W)) * (h | (A \ hW))) by A39, RELAT_1:36

.= F * (((h ") * (id (B \ W))) * (h | (A \ hW))) by RELAT_1:65

.= F * ((h ") * ((id (B \ W)) * (h | (A \ hW)))) by RELAT_1:36

.= F * ((h ") * (h | (A \ hW))) by A41, RELAT_1:53

.= F * (((h ") * h) | (A \ hW)) by RELAT_1:83

.= (F * ((h ") * h)) | (A \ hW) by RELAT_1:83

.= (F * (id A)) | (A \ hW) by TOPS_2:52, A8, A10, A5, A9

.= F | (dom F) by A40, XBOOLE_1:36, RELAT_1:51

.= F ;

hence contradiction by A38, A29; :: thesis: verum

end;A35: ((TOP-REAL n) | B) | bw = (TOP-REAL n) | (B \ W) by PRE_TOPC:7, XBOOLE_1:36;

A36: ((TOP-REAL n) | A) | ((h ") .: (B \ W)) = (TOP-REAL n) | (A \ hW) by A31, PRE_TOPC:7, A7;

then reconsider HBW = hbw as Function of ((TOP-REAL n) | (B \ W)),((TOP-REAL n) | (A \ hW)) by A35;

reconsider fhW = F * HBW as Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) by A34;

take fhW ; :: thesis: ( fhW is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> fhW ) )

thus fhW is continuous by A34, JORDAN24:13, A6, A2, A3, A12, A36, A35, A28, TOPS_2:46; :: thesis: for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds

h | (B \ W) <> fhW

let g be Function of ((TOP-REAL n) | B),(Tunit_circle n); :: thesis: ( g is continuous implies g | (B \ W) <> fhW )

assume A37: g is continuous ; :: thesis: g | (B \ W) <> fhW

reconsider gh = g * h as Function of ((TOP-REAL n) | A),(Tunit_circle n) by A12;

A38: gh is continuous by A5, A12, A37, TOPS_2:46;

assume A39: g | (B \ W) = fhW ; :: thesis: contradiction

A40: dom F = A \ hW by FUNCT_2:def 1, A11, A27;

A41: rng (h | (A \ hW)) = h .: (A \ hW) by RELAT_1:115

.= h .: (h " (B \ W)) by TOPS_2:55, A9, A10, A31, A5, A30

.= B \ W by FUNCT_1:77, A10, XBOOLE_1:36 ;

gh | (A \ hW) = g * (h | (A \ hW)) by RELAT_1:83

.= g * ((id (B \ W)) * (h | (A \ hW))) by A41, RELAT_1:53

.= (g * (id (B \ W))) * (h | (A \ hW)) by RELAT_1:36

.= (g | (B \ W)) * (h | (A \ hW)) by RELAT_1:65

.= F * (((h ") | (B \ W)) * (h | (A \ hW))) by A39, RELAT_1:36

.= F * (((h ") * (id (B \ W))) * (h | (A \ hW))) by RELAT_1:65

.= F * ((h ") * ((id (B \ W)) * (h | (A \ hW)))) by RELAT_1:36

.= F * ((h ") * (h | (A \ hW))) by A41, RELAT_1:53

.= F * (((h ") * h) | (A \ hW)) by RELAT_1:83

.= (F * ((h ") * h)) | (A \ hW) by RELAT_1:83

.= (F * (id A)) | (A \ hW) by TOPS_2:52, A8, A10, A5, A9

.= F | (dom F) by A40, XBOOLE_1:36, RELAT_1:51

.= F ;

hence contradiction by A38, A29; :: thesis: verum

then hp in B \ (Fr B) by A12, A9, XBOOLE_0:def 5;

hence h . p in Int B by TOPS_1:40; :: thesis: verum