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

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

let A, B be Subset of (); :: thesis: ( B is closed & p in Int A implies for h being Function of (() | A),(() | 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 (() | A),(() | 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 (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
let h be Function of (() | A),(() | 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 ;
A7: [#] (() | A) = A by PRE_TOPC:def 5;
then A8: dom h = A by ;
A9: [#] (() | B) = B by PRE_TOPC:def 5;
then A10: rng h = B by ;
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: h . p in Int B
hence h . p in Int B by Lm3, A2, A5; :: thesis: verum
end;
suppose A11: n > 0 ; :: thesis: h . p in Int B
A12: h . p in rng h by ;
then reconsider hp = h . p as Point of () by A10;
ex r being Real st
( r > 0 & ( for U being open Subset of (() | B) st hp in U & U c= Ball (hp,r) holds
ex f being Function of (() | (B \ U)),() st
( f is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ U) <> f ) ) ) )
proof
reconsider hP = hp as Point of () by ;
not p in Fr A by ;
then consider r being Real such that
A14: r > 0 and
A15: for U being open Subset of (() | A) st p in U & U c= Ball (p,r) holds
ex f being Function of (() | (A \ U)),() st
( f is continuous & ( for h being Function of (() | A),() st h is continuous holds
h | (A \ U) <> f ) ) by A11, A2, A3, Th8;
reconsider BA = (Ball (p,r)) /\ A as Subset of (() | A) by ;
Ball (p,r) in the topology of () by PRE_TOPC:def 2;
then BA in the topology of (() | A) by ;
then reconsider BA = BA as open Subset of (() | A) by PRE_TOPC:def 2;
h .: BA is open by ;
then h .: BA in the topology of (() | B) by PRE_TOPC:def 2;
then consider U being Subset of () such that
A16: U in the topology of () and
A17: h .: BA = U /\ ([#] (() | B)) by PRE_TOPC:def 4;
reconsider U = U as open Subset of () by ;
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 ;
then hp in h .: BA by ;
then hp in U by ;
then consider s being Real such that
A19: s > 0 and
A20: Ball (hP,s) c= U by ;
take s ; :: thesis: ( s > 0 & ( for U being open Subset of (() | B) st hp in U & U c= Ball (hp,s) holds
ex f being Function of (() | (B \ U)),() st
( f is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ U) <> f ) ) ) )

thus s > 0 by A19; :: thesis: for U being open Subset of (() | B) st hp in U & U c= Ball (hp,s) holds
ex f being Function of (() | (B \ U)),() st
( f is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ U) <> f ) )

let W be open Subset of (() | B); :: thesis: ( hp in W & W c= Ball (hp,s) implies ex f being Function of (() | (B \ W)),() st
( f is continuous & ( for h being Function of (() | B),() 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 (() | (B \ W)),() st
( f is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ W) <> f ) )

A23: W /\ B = W by ;
Ball (hp,s) = Ball (hP,s) by TOPREAL9:13;
then W c= U by ;
then A24: W c= U /\ B by ;
h " (U /\ B) = h " (h .: BA) by
.= BA by ;
then A25: h " W c= BA by ;
reconsider hW = h " W as open Subset of (() | A) by ;
A26: BA c= Ball (p,r) by XBOOLE_1:17;
set BW = B \ W;
reconsider bw = B \ W as Subset of (() | B) by ;
A27: [#] (() | (A \ hW)) = A \ hW by PRE_TOPC:def 5;
p in h " W by ;
then consider F being Function of (() | (A \ hW)),() such that
A28: F is continuous and
A29: for h being Function of (() | A),() st h is continuous holds
h | (A \ hW) <> F by ;
A30: B \ W c= B by XBOOLE_1:36;
then A31: (h ") .: (B \ W) = h " (B \ W) by
.= (h " B) \ hW by FUNCT_1:69
.= A \ hW by ;
per cases ( A \ hW is empty or not A \ hW is empty ) ;
suppose A32: A \ hW is empty ; :: thesis: ex f being Function of (() | (B \ W)),() st
( f is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ W) <> f ) )

reconsider n1 = n - 1 as Element of NAT by ;
set h = the continuous Function of (() | A),(Tunit_circle (n1 + 1));
reconsider H = the continuous Function of (() | A),(Tunit_circle (n1 + 1)) as Function of (() | A),() ;
A33: H | (A \ hW) = {} by A32;
H | (A \ hW) <> F by A29;
hence ex f being Function of (() | (B \ W)),() st
( f is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ W) <> f ) ) by ; :: thesis: verum
end;
suppose A34: not A \ hW is empty ; :: thesis: ex f being Function of (() | (B \ W)),() st
( f is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ W) <> f ) )

reconsider hbw = (h ") | (B \ W) as Function of ((() | B) | bw),((() | A) | ((h ") .: (B \ W))) by ;
A35: ((TOP-REAL n) | B) | bw = () | (B \ W) by ;
A36: ((TOP-REAL n) | A) | ((h ") .: (B \ W)) = () | (A \ hW) by ;
then reconsider HBW = hbw as Function of (() | (B \ W)),(() | (A \ hW)) by A35;
reconsider fhW = F * HBW as Function of (() | (B \ W)),() by A34;
take fhW ; :: thesis: ( fhW is continuous & ( for h being Function of (() | B),() st h is continuous holds
h | (B \ W) <> fhW ) )

thus fhW is continuous by ; :: thesis: for h being Function of (() | B),() st h is continuous holds
h | (B \ W) <> fhW

let g be Function of (() | B),(); :: 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 (() | A),() by A12;
A38: gh is continuous by ;
assume A39: g | (B \ W) = fhW ; :: thesis: contradiction
A40: dom F = A \ hW by ;
A41: rng (h | (A \ hW)) = h .: (A \ hW) by RELAT_1:115
.= h .: (h " (B \ W)) by
.= B \ W by ;
gh | (A \ hW) = g * (h | (A \ hW)) by RELAT_1:83
.= g * ((id (B \ W)) * (h | (A \ hW))) by
.= (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
.= 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
.= F * (((h ") * h) | (A \ hW)) by RELAT_1:83
.= (F * ((h ") * h)) | (A \ hW) by RELAT_1:83
.= (F * (id A)) | (A \ hW) by
.= F | (dom F) by
.= F ;
hence contradiction by A38, A29; :: thesis: verum
end;
end;
end;
then not hp in Fr B by ;
then hp in B \ (Fr B) by ;
hence h . p in Int B by TOPS_1:40; :: thesis: verum
end;
end;