let n be Nat; :: thesis: for A being Subset of ()
for p being Point of () st p in Fr A & A is closed holds
for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) )

let A be Subset of (); :: thesis: for p being Point of () st p in Fr A & A is closed holds
for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) )

set TR = TOP-REAL n;
let p be Point of (); :: thesis: ( p in Fr A & A is closed implies for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) ) )

assume that
A1: p in Fr A and
A2: A is closed ; :: thesis: for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) )

A3: Fr A c= A by ;
n > 0
proof
assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
then A4: the carrier of () = {(0. ())} by ;
[#] () is open ;
hence contradiction by A4, A1, ZFMISC_1:33; :: thesis: verum
end;
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
set TU = Tunit_circle n;
A5: p is Element of REAL n by EUCLID:22;
let r be Real; :: thesis: ( r > 0 implies ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) ) )

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

set r3 = r / 3;
set r2 = 2 * (r / 3);
set B = Ball (p,(r / 3));
p is Element of REAL n by EUCLID:22;
then |.(p - p).| = 0 ;
then p in Ball (p,(r / 3)) by A6;
then A ` meets Ball (p,(r / 3)) by ;
then consider x being object such that
A7: x in A ` and
A8: x in Ball (p,(r / 3)) by XBOOLE_0:3;
reconsider x = x as Element of () by A7;
set u = Ball (x,(2 * (r / 3)));
set clU = cl_Ball (x,(2 * (r / 3)));
A9: n in NAT by ORDINAL1:def 12;
A10: Ball (x,(2 * (r / 3))) c= cl_Ball (x,(2 * (r / 3))) by TOPREAL9:16;
A11: [#] (() | A) = A by PRE_TOPC:def 5;
then reconsider U = (Ball (x,(2 * (r / 3)))) /\ A as Subset of (() | A) by XBOOLE_1:17;
Ball (x,(2 * (r / 3))) in the topology of () by PRE_TOPC:def 2;
then U in the topology of (() | A) by ;
then reconsider U = U as open Subset of (() | A) by PRE_TOPC:def 2;
take U ; :: thesis: ( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) )

x is Element of REAL n by EUCLID:22;
then A12: |.(x - p).| = |.(p - x).| by ;
|.(x - p).| + (2 * (r / 3)) < (r / 3) + (2 * (r / 3)) by ;
then A13: Ball (x,(2 * (r / 3))) c= Ball (p,r) by Th5;
2 * (r / 3) > r / 3 by ;
then |.(x - p).| < 2 * (r / 3) by ;
then A14: p in Ball (x,(2 * (r / 3))) by A12;
hence p in U by ; :: thesis: ( U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) )

U c= Ball (x,(2 * (r / 3))) by XBOOLE_1:17;
hence U c= Ball (p,r) by A13; :: thesis: for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f )

let f be Function of (() | (A \ U)),(); :: thesis: ( f is continuous implies ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) )

assume A15: f is continuous ; :: thesis: ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f )

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

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),() ;
take H ; :: thesis: ( H is continuous & H | (A \ U) = f )
f = {} by A16;
hence ( H is continuous & H | (A \ U) = f ) by A16; :: thesis: verum
end;
suppose A17: not A \ U is empty ; :: thesis: ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f )

set S = Sphere (x,(2 * (r / 3)));
reconsider AUS = (A \ U) \/ (Sphere (x,(2 * (r / 3)))) as non empty Subset of () by A17;
A18: ( (TOP-REAL n) | AUS is metrizable & () | AUS is finite-ind & () | AUS is second-countable )
proof
reconsider aus = AUS as Subset of TopStruct(# the carrier of (), the topology of () #) ;
A19: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
(TOP-REAL n) | AUS = TopStruct(# the carrier of (), the topology of () #) | aus by PRE_TOPC:36;
hence ( (TOP-REAL n) | AUS is metrizable & () | AUS is finite-ind & () | AUS is second-countable ) by A19; :: thesis: verum
end;
A20: [#] (() | AUS) = AUS by PRE_TOPC:def 5;
then reconsider AU = A \ U, SS = Sphere (x,(2 * (r / 3))) as Subset of (() | AUS) by XBOOLE_1:7;
AU ` = AUS \ AU by
.= (Sphere (x,(2 * (r / 3)))) \ AU by XBOOLE_1:40 ;
then A21: AU ` c= SS by XBOOLE_1:36;
ind (Sphere (x,(2 * (r / 3)))) = n1 by ;
then ind SS = n1 by TOPDIM_1:21;
then A22: ind (AU `) <= n1 by ;
A23: (TOP-REAL n) | (A \ U) = (() | AUS) | AU by ;
then reconsider F = f as Function of ((() | AUS) | AU),() ;
A \ U = A \ (Ball (x,(2 * (r / 3)))) by XBOOLE_1:47;
then A24: A \ U is closed by ;
then AU is closed by TSEP_1:8;
then consider g being continuous Function of (() | AUS),(Tunit_circle (n1 + 1)) such that
A25: g | AU = F by Th3, A23, A15, A18, A22;
A26: [#] (() | A) = A by PRE_TOPC:def 5;
then reconsider AclU = A /\ (cl_Ball (x,(2 * (r / 3)))), au = A \ U as Subset of (() | A) by ;
set T3 = (() | A) | AclU;
set T4 = (() | A) | au;
A27: (A /\ U) \/ au = A by XBOOLE_1:51;
A ` = ([#] ()) \ A by SUBSET_1:def 4;
then not x in A by ;
then consider h being Function of (() | A),(() | (Sphere (x,(2 * (r / 3))))) such that
A28: h is continuous and
A29: h | (Sphere (x,(2 * (r / 3)))) = id (A /\ (Sphere (x,(2 * (r / 3))))) by ;
A30: n1 + 1 = n ;
then A31: dom h = the carrier of (() | A) by ;
A32: [#] (() | (Sphere (x,(2 * (r / 3))))) = Sphere (x,(2 * (r / 3))) by PRE_TOPC:def 5;
then rng h c= the carrier of () by XBOOLE_1:1;
then reconsider h1 = h as Function of (() | A),() by ;
A33: Sphere (x,(2 * (r / 3))) c= AUS by XBOOLE_1:7;
rng h c= [#] (() | (Sphere (x,(2 * (r / 3))))) ;
then reconsider h2 = h1 as Function of (() | A),(() | AUS) by ;
h1 is continuous by ;
then A34: h2 is continuous by PRE_TOPC:27;
set T2 = (() | AUS) | AU;
A35: ((TOP-REAL n) | AUS) | AU = () | (A \ U) by ;
A36: (cl_Ball (x,(2 * (r / 3)))) \ (Ball (x,(2 * (r / 3)))) = Sphere (x,(2 * (r / 3))) by ;
A37: (A /\ A) /\ (Ball (x,(2 * (r / 3)))) = A /\ (A /\ (Ball (x,(2 * (r / 3))))) by XBOOLE_1:16;
A38: g | ((() | AUS) | AU) = g | the carrier of ((() | AUS) | AU) by TMAP_1:def 4;
((TOP-REAL n) | A) | au = () | (A \ U) by ;
then reconsider gT2 = g | ((() | AUS) | AU) as continuous Function of ((() | A) | au),(Tunit_circle (n1 + 1)) by ;
A39: [#] ((() | A) | AclU) = AclU by PRE_TOPC:def 5;
not AclU is empty by ;
then reconsider gh2T3 = g * (h2 | ((() | A) | AclU)) as continuous Function of ((() | A) | AclU),(Tunit_circle (n1 + 1)) by A34;
A40: [#] ((() | A) | au) = au by PRE_TOPC:def 5;
A41: h2 | ((() | A) | AclU) = h2 | the carrier of ((() | A) | AclU) by ;
A42: now :: thesis: for x being object st x in (dom gh2T3) /\ (dom gT2) holds
gh2T3 . x = gT2 . x
let x be object ; :: thesis: ( x in (dom gh2T3) /\ (dom gT2) implies gh2T3 . x = gT2 . x )
assume A43: x in (dom gh2T3) /\ (dom gT2) ; :: thesis: gh2T3 . x = gT2 . x
A44: not x in U by ;
x in A by ;
then A45: not x in Ball (x,(2 * (r / 3))) by ;
A46: x in dom gh2T3 by ;
then x in cl_Ball (x,(2 * (r / 3))) by ;
then A47: x in Sphere (x,(2 * (r / 3))) by ;
A48: x in dom gT2 by ;
x in A by ;
then A49: x in A /\ (Sphere (x,(2 * (r / 3)))) by ;
x in dom (h2 | ((() | A) | AclU)) by ;
then (h2 | ((() | A) | AclU)) . x = h2 . x by
.= (h | (Sphere (x,(2 * (r / 3))))) . x by
.= x by ;
hence gh2T3 . x = g . x by
.= gT2 . x by ;
:: thesis: verum
end;
A50: AclU is closed by ;
au is closed by ;
then reconsider G = gh2T3 +* gT2 as continuous Function of ((() | A) | (AclU \/ au)),(Tunit_circle (n1 + 1)) by ;
W: A /\ (Ball (x,(2 * (r / 3)))) c= AclU by ;
A = AclU \/ au by ;
then A51: ((TOP-REAL n) | A) | (AclU \/ au) = () | A by ;
then reconsider GG = G as Function of (() | A),() ;
take GG ; :: thesis: ( GG is continuous & GG | (A \ U) = f )
thus GG is continuous by A51; :: thesis: GG | (A \ U) = f
A52: [#] (() | (A \ U)) = A \ U by PRE_TOPC:def 5;
A53: dom gT2 = the carrier of ((() | A) | au) by FUNCT_2:def 1;
A54: now :: thesis: for x being set st x in dom f holds
(GG | (A \ U)) . x = f . x
let x be set ; :: thesis: ( x in dom f implies (GG | (A \ U)) . x = f . x )
assume A55: x in dom f ; :: thesis: (GG | (A \ U)) . x = f . x
hence (GG | (A \ U)) . x = GG . x by
.= gT2 . x by
.= g . x by
.= f . x by ;
:: thesis: verum
end;
dom GG = A by ;
then A56: dom (GG | (A \ U)) = A /\ (A \ U) by RELAT_1:61
.= A \ U by ;
dom f = A \ U by ;
hence GG | (A \ U) = f by ; :: thesis: verum
end;
end;