let n be Nat; :: thesis: for p being Point of ()
for A, B being Subset of () st A is closed & p in Fr A holds
for h being Function of (() | A),(() | B) st h is being_homeomorphism holds
h . p in Fr B

let p be Point of (); :: thesis: for A, B being Subset of () st A is closed & p in Fr A holds
for h being Function of (() | A),(() | B) st h is being_homeomorphism holds
h . p in Fr B

let A, B be Subset of (); :: thesis: ( A is closed & p in Fr A implies for h being Function of (() | A),(() | 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 (() | A),(() | B) st h is being_homeomorphism holds
h . p in Fr B

A3: Fr A c= A by ;
let h be Function of (() | A),(() | 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: [#] (() | A) = A by PRE_TOPC:def 5;
then A6: dom h = A by ;
then A7: h . p in rng h by ;
A8: [#] (() | B) = B by PRE_TOPC:def 5;
then A9: rng h = B by ;
then reconsider hp = h . p as Point of () by A7;
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: h . p in Fr B
hence h . p in Fr B by Lm3, A4, A2; :: thesis: verum
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 (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
for r being Real st r > 0 holds
ex U being open Subset of (() | B) st
( hp in U & U c= Ball (hp,r) & ( for f being Function of (() | (B \ U)),() st f is continuous holds
ex h being Function of (() | B),() st
( h is continuous & h | (B \ U) = f ) ) )
proof
reconsider P = p as Point of () by ;
let r be Real; :: thesis: ( r > 0 implies ex U being open Subset of (() | B) st
( hp in U & U c= Ball (hp,r) & ( for f being Function of (() | (B \ U)),() st f is continuous holds
ex h being Function of (() | B),() st
( h is continuous & h | (B \ U) = f ) ) ) )

assume A13: r > 0 ; :: thesis: ex U being open Subset of (() | B) st
( hp in U & U c= Ball (hp,r) & ( for f being Function of (() | (B \ U)),() st f is continuous holds
ex h being Function of (() | B),() st
( h is continuous & h | (B \ U) = f ) ) )

reconsider BB = B /\ (Ball (hp,r)) as Subset of (() | B) by ;
Ball (hp,r) in the topology of () by PRE_TOPC:def 2;
then BB in the topology of (() | B) by ;
then reconsider BB = BB as open Subset of (() | B) by PRE_TOPC:def 2;
h " BB is open by ;
then h " BB in the topology of (() | A) by PRE_TOPC:def 2;
then consider U being Subset of () such that
A14: U in the topology of () and
A15: h " BB = U /\ ([#] (() | A)) by PRE_TOPC:def 4;
reconsider U = U as open Subset of () by ;
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 ;
then p in h " BB by ;
then p in U by ;
then consider s being Real such that
A17: s > 0 and
A18: Ball (P,s) c= U by ;
consider W being open Subset of (() | A) such that
A19: p in W and
A20: W c= Ball (p,s) and
A21: for f being Function of (() | (A \ W)),() st f is continuous holds
ex h being Function of (() | A),() 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 ;
W /\ A = W by ;
then W c= (Ball (p,s)) /\ A by ;
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 ;
not (TOP-REAL n) | B is empty by A3, A2, A6;
then reconsider hW = h .: W as open Subset of (() | B) by ;
take hW ; :: thesis: ( hp in hW & hW c= Ball (hp,r) & ( for f being Function of (() | (B \ hW)),() st f is continuous holds
ex h being Function of (() | B),() 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 ; :: thesis: for f being Function of (() | (B \ hW)),() st f is continuous holds
ex h being Function of (() | B),() st
( h is continuous & h | (B \ hW) = f )

set AW = A \ W;
set haw = h | (A \ W);
set T = Tunit_circle n;
A24: [#] (() | (B \ hW)) = B \ hW by PRE_TOPC:def 5;
reconsider aw = A \ W as Subset of (() | A) by ;
let f be Function of (() | (B \ hW)),(); :: thesis: ( f is continuous implies ex h being Function of (() | B),() st
( h is continuous & h | (B \ hW) = f ) )

assume A25: f is continuous ; :: thesis: ex h being Function of (() | B),() st
( h is continuous & h | (B \ hW) = f )

per cases ( B \ hW is empty or not B \ hW is empty ) ;
suppose A26: B \ hW is empty ; :: thesis: ex h being Function of (() | B),() st
( h is continuous & h | (B \ hW) = f )

set h = the continuous Function of (() | B),(Tunit_circle (n1 + 1));
reconsider H = the continuous Function of (() | B),(Tunit_circle (n1 + 1)) as Function of (() | B),() ;
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;
suppose A27: not B \ hW is empty ; :: thesis: ex h being Function of (() | B),() st
( 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 ((() | A) | aw),((() | B) | (h .: (A \ W))) by ;
A28: h .: (A \ W) = (h .: A) \ (h .: W) by
.= B \ hW by ;
then A29: ((TOP-REAL n) | B) | (h .: (A \ W)) = () | (B \ hW) by ;
A30: ((TOP-REAL n) | A) | aw = () | (A \ W) by ;
then reconsider HAW = haw as Function of (() | (A \ W)),(() | (B \ hW)) by A29;
reconsider fhW = f * HAW as Function of (() | (A \ W)),() by A27;
fhW is continuous by ;
then consider HW being Function of (() | A),() such that
A31: HW is continuous and
A32: HW | (A \ W) = fhW by A21;
reconsider HWh = HW * (h ") as Function of (() | B),() by A3, A2;
take HWh ; :: thesis: ( HWh is continuous & HWh | (B \ hW) = f )
h " is continuous by ;
hence HWh is continuous by ; :: thesis: HWh | (B \ hW) = f
A33: dom f = B \ hW by ;
A34: rng ((h ") | (B \ hW)) = (h ") .: (B \ hW) by RELAT_1:115
.= h " (h .: (A \ W)) by
.= A \ W by ;
thus HWh | (B \ hW) = HW * ((h ") | (B \ hW)) by RELAT_1:83
.= HW * ((id (A \ W)) * ((h ") | (B \ hW))) by
.= (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
.= ((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
.= ((f * h) * (h ")) | (B \ hW) by RELAT_1:83
.= (f * (h * (h "))) | (B \ hW) by RELAT_1:36
.= (f * (id B)) | (B \ hW) by
.= f | (dom f) by
.= f ; :: thesis: verum
end;
end;
end;
hence h . p in Fr B by Th8, A7, A8, A10; :: thesis: verum
end;
end;