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

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

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

h . p in Fr B

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

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

h . p in Fr B

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

h . p in Fr B )

set TRn = TOP-REAL n;

assume that

A1: A is closed and

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

h . p in Fr B

A3: Fr A c= A by A1, TOPS_1:35;

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

assume A4: h is being_homeomorphism ; :: thesis: h . p in Fr B

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

then A6: dom h = A by A4, TOPS_2:def 5;

then A7: h . p in rng h by A3, A2, FUNCT_1:def 3;

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

then A9: rng h = B by A4, TOPS_2:def 5;

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

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

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

h . p in Fr B

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

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

h . p in Fr B

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

h . p in Fr B )

set TRn = TOP-REAL n;

assume that

A1: A is closed and

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

h . p in Fr B

A3: Fr A c= A by A1, TOPS_1:35;

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

assume A4: h is being_homeomorphism ; :: thesis: h . p in Fr B

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

then A6: dom h = A by A4, TOPS_2:def 5;

then A7: h . p in rng h by A3, A2, FUNCT_1:def 3;

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

then A9: rng h = B by A4, TOPS_2:def 5;

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

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

end;

suppose A10:
n > 0
; :: thesis: h . p in Fr B

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

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

for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | B) st

( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ U) = f ) ) )

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

for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | B) st

( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ U) = f ) ) )

proof

hence
h . p in Fr B
by Th8, A7, A8, A10; :: thesis: verum
reconsider P = p as Point of (Euclid n) by A11, TOPMETR:12;

let r be Real; :: thesis: ( r > 0 implies ex U being open Subset of ((TOP-REAL n) | B) st

( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ U) = f ) ) ) )

assume A13: r > 0 ; :: thesis: ex U being open Subset of ((TOP-REAL n) | B) st

( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ U) = f ) ) )

reconsider BB = B /\ (Ball (hp,r)) as Subset of ((TOP-REAL n) | B) by A8, XBOOLE_1:17;

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

then BB in the topology of ((TOP-REAL n) | B) by A8, PRE_TOPC:def 4;

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

h " BB is open by A7, A4, A8, TOPS_2:43;

then h " BB in the topology of ((TOP-REAL n) | A) by PRE_TOPC:def 2;

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

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

A15: h " BB = U /\ ([#] ((TOP-REAL n) | A)) by PRE_TOPC:def 4;

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

A16: Int U = U by TOPS_1:23;

hp is Element of REAL n by EUCLID:22;

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

then hp in Ball (hp,r) by A13;

then hp in BB by A7, A8, XBOOLE_0:def 4;

then p in h " BB by A3, A2, A6, FUNCT_1:def 7;

then p in U by A15, XBOOLE_0:def 4;

then consider s being Real such that

A17: s > 0 and

A18: Ball (P,s) c= U by A16, GOBOARD6:5;

consider W being open Subset of ((TOP-REAL n) | A) such that

A19: p in W and

A20: W c= Ball (p,s) and

A21: for f being Function of ((TOP-REAL n) | (A \ W)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ W) = f ) by A1, A17, Th9, A2;

Ball (p,s) = Ball (P,s) by TOPREAL9:13;

then A22: (Ball (p,s)) /\ A c= U /\ A by A18, XBOOLE_1:27;

W /\ A = W by A5, XBOOLE_1:28;

then W c= (Ball (p,s)) /\ A by A20, XBOOLE_1:27;

then W c= U /\ A by A22;

then h .: W c= h .: (U /\ A) by RELAT_1:123;

then A23: h .: W c= BB by FUNCT_1:77, A8, A9, A15, A5;

not (TOP-REAL n) | B is empty by A3, A2, A6;

then reconsider hW = h .: W as open Subset of ((TOP-REAL n) | B) by A3, A2, A4, TOPGRP_1:25;

take hW ; :: thesis: ( hp in hW & hW c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f ) ) )

BB c= Ball (hp,r) by XBOOLE_1:17;

hence ( hp in hW & hW c= Ball (hp,r) ) by A3, A2, A6, FUNCT_1:def 6, A19, A23; :: thesis: for f being Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f )

set AW = A \ W;

set haw = h | (A \ W);

set T = Tunit_circle n;

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

reconsider aw = A \ W as Subset of ((TOP-REAL n) | A) by XBOOLE_1:36, A5;

let f be Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n); :: thesis: ( f is continuous implies ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f ) )

assume A25: f is continuous ; :: thesis: ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f )

end;let r be Real; :: thesis: ( r > 0 implies ex U being open Subset of ((TOP-REAL n) | B) st

( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ U) = f ) ) ) )

assume A13: r > 0 ; :: thesis: ex U being open Subset of ((TOP-REAL n) | B) st

( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ U) = f ) ) )

reconsider BB = B /\ (Ball (hp,r)) as Subset of ((TOP-REAL n) | B) by A8, XBOOLE_1:17;

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

then BB in the topology of ((TOP-REAL n) | B) by A8, PRE_TOPC:def 4;

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

h " BB is open by A7, A4, A8, TOPS_2:43;

then h " BB in the topology of ((TOP-REAL n) | A) by PRE_TOPC:def 2;

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

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

A15: h " BB = U /\ ([#] ((TOP-REAL n) | A)) by PRE_TOPC:def 4;

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

A16: Int U = U by TOPS_1:23;

hp is Element of REAL n by EUCLID:22;

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

then hp in Ball (hp,r) by A13;

then hp in BB by A7, A8, XBOOLE_0:def 4;

then p in h " BB by A3, A2, A6, FUNCT_1:def 7;

then p in U by A15, XBOOLE_0:def 4;

then consider s being Real such that

A17: s > 0 and

A18: Ball (P,s) c= U by A16, GOBOARD6:5;

consider W being open Subset of ((TOP-REAL n) | A) such that

A19: p in W and

A20: W c= Ball (p,s) and

A21: for f being Function of ((TOP-REAL n) | (A \ W)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ W) = f ) by A1, A17, Th9, A2;

Ball (p,s) = Ball (P,s) by TOPREAL9:13;

then A22: (Ball (p,s)) /\ A c= U /\ A by A18, XBOOLE_1:27;

W /\ A = W by A5, XBOOLE_1:28;

then W c= (Ball (p,s)) /\ A by A20, XBOOLE_1:27;

then W c= U /\ A by A22;

then h .: W c= h .: (U /\ A) by RELAT_1:123;

then A23: h .: W c= BB by FUNCT_1:77, A8, A9, A15, A5;

not (TOP-REAL n) | B is empty by A3, A2, A6;

then reconsider hW = h .: W as open Subset of ((TOP-REAL n) | B) by A3, A2, A4, TOPGRP_1:25;

take hW ; :: thesis: ( hp in hW & hW c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f ) ) )

BB c= Ball (hp,r) by XBOOLE_1:17;

hence ( hp in hW & hW c= Ball (hp,r) ) by A3, A2, A6, FUNCT_1:def 6, A19, A23; :: thesis: for f being Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f )

set AW = A \ W;

set haw = h | (A \ W);

set T = Tunit_circle n;

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

reconsider aw = A \ W as Subset of ((TOP-REAL n) | A) by XBOOLE_1:36, A5;

let f be Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n); :: thesis: ( f is continuous implies ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f ) )

assume A25: f is continuous ; :: thesis: ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f )

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

end;

suppose A26:
B \ hW is empty
; :: thesis: ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st

( h is continuous & h | (B \ hW) = f )

( h is continuous & h | (B \ hW) = f )

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

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

take H ; :: thesis: ( H is continuous & H | (B \ hW) = f )

f = {} by A26;

hence ( H is continuous & H | (B \ hW) = f ) by A26; :: thesis: verum

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

take H ; :: thesis: ( H is continuous & H | (B \ hW) = f )

f = {} by A26;

hence ( H is continuous & H | (B \ hW) = f ) by A26; :: thesis: verum

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

( h is continuous & h | (B \ hW) = f )

( h is continuous & h | (B \ hW) = f )

set AW = A \ W;

set haw = h | (A \ W);

set T = Tunit_circle n;

reconsider haw = h | (A \ W) as Function of (((TOP-REAL n) | A) | aw),(((TOP-REAL n) | B) | (h .: (A \ W))) by A3, A2, A7, JORDAN24:12;

A28: h .: (A \ W) = (h .: A) \ (h .: W) by A4, FUNCT_1:64

.= B \ hW by RELAT_1:113, A6, A9 ;

then A29: ((TOP-REAL n) | B) | (h .: (A \ W)) = (TOP-REAL n) | (B \ hW) by XBOOLE_1:36, PRE_TOPC:7;

A30: ((TOP-REAL n) | A) | aw = (TOP-REAL n) | (A \ W) by PRE_TOPC:7, XBOOLE_1:36;

then reconsider HAW = haw as Function of ((TOP-REAL n) | (A \ W)),((TOP-REAL n) | (B \ hW)) by A29;

reconsider fhW = f * HAW as Function of ((TOP-REAL n) | (A \ W)),(Tunit_circle n) by A27;

fhW is continuous by A27, JORDAN24:13, A4, A3, A2, A7, A29, A30, A25, TOPS_2:46;

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

A31: HW is continuous and

A32: HW | (A \ W) = fhW by A21;

reconsider HWh = HW * (h ") as Function of ((TOP-REAL n) | B),(Tunit_circle n) by A3, A2;

take HWh ; :: thesis: ( HWh is continuous & HWh | (B \ hW) = f )

h " is continuous by A4, TOPS_2:def 5;

hence HWh is continuous by TOPS_2:46, A3, A2, A31; :: thesis: HWh | (B \ hW) = f

A33: dom f = B \ hW by A10, A24, FUNCT_2:def 1;

A34: rng ((h ") | (B \ hW)) = (h ") .: (B \ hW) by RELAT_1:115

.= h " (h .: (A \ W)) by A28, A8, A9, A4, TOPS_2:55

.= A \ W by FUNCT_1:94, A6, A4, XBOOLE_1:36 ;

thus HWh | (B \ hW) = HW * ((h ") | (B \ hW)) by RELAT_1:83

.= HW * ((id (A \ W)) * ((h ") | (B \ hW))) by A34, RELAT_1:53

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

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

.= ((f * h) | (A \ W)) * ((h ") | (B \ hW)) by A32, RELAT_1:83

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

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

.= (f * h) * ((h ") | (B \ hW)) by A34, RELAT_1:53

.= ((f * h) * (h ")) | (B \ hW) by RELAT_1:83

.= (f * (h * (h "))) | (B \ hW) by RELAT_1:36

.= (f * (id B)) | (B \ hW) by TOPS_2:52, A9, A4, A8

.= f | (dom f) by A33, XBOOLE_1:36, RELAT_1:51

.= f ; :: thesis: verum

end;set haw = h | (A \ W);

set T = Tunit_circle n;

reconsider haw = h | (A \ W) as Function of (((TOP-REAL n) | A) | aw),(((TOP-REAL n) | B) | (h .: (A \ W))) by A3, A2, A7, JORDAN24:12;

A28: h .: (A \ W) = (h .: A) \ (h .: W) by A4, FUNCT_1:64

.= B \ hW by RELAT_1:113, A6, A9 ;

then A29: ((TOP-REAL n) | B) | (h .: (A \ W)) = (TOP-REAL n) | (B \ hW) by XBOOLE_1:36, PRE_TOPC:7;

A30: ((TOP-REAL n) | A) | aw = (TOP-REAL n) | (A \ W) by PRE_TOPC:7, XBOOLE_1:36;

then reconsider HAW = haw as Function of ((TOP-REAL n) | (A \ W)),((TOP-REAL n) | (B \ hW)) by A29;

reconsider fhW = f * HAW as Function of ((TOP-REAL n) | (A \ W)),(Tunit_circle n) by A27;

fhW is continuous by A27, JORDAN24:13, A4, A3, A2, A7, A29, A30, A25, TOPS_2:46;

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

A31: HW is continuous and

A32: HW | (A \ W) = fhW by A21;

reconsider HWh = HW * (h ") as Function of ((TOP-REAL n) | B),(Tunit_circle n) by A3, A2;

take HWh ; :: thesis: ( HWh is continuous & HWh | (B \ hW) = f )

h " is continuous by A4, TOPS_2:def 5;

hence HWh is continuous by TOPS_2:46, A3, A2, A31; :: thesis: HWh | (B \ hW) = f

A33: dom f = B \ hW by A10, A24, FUNCT_2:def 1;

A34: rng ((h ") | (B \ hW)) = (h ") .: (B \ hW) by RELAT_1:115

.= h " (h .: (A \ W)) by A28, A8, A9, A4, TOPS_2:55

.= A \ W by FUNCT_1:94, A6, A4, XBOOLE_1:36 ;

thus HWh | (B \ hW) = HW * ((h ") | (B \ hW)) by RELAT_1:83

.= HW * ((id (A \ W)) * ((h ") | (B \ hW))) by A34, RELAT_1:53

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

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

.= ((f * h) | (A \ W)) * ((h ") | (B \ hW)) by A32, RELAT_1:83

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

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

.= (f * h) * ((h ") | (B \ hW)) by A34, RELAT_1:53

.= ((f * h) * (h ")) | (B \ hW) by RELAT_1:83

.= (f * (h * (h "))) | (B \ hW) by RELAT_1:36

.= (f * (id B)) | (B \ hW) by TOPS_2:52, A9, A4, A8

.= f | (dom f) by A33, XBOOLE_1:36, RELAT_1:51

.= f ; :: thesis: verum