let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)

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

for r being Real st r > 0 holds

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

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

for r being Real st r > 0 holds

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

set TR = TOP-REAL n;

let p be Point of (TOP-REAL n); :: thesis: ( p in Fr A & A is closed implies for r being Real st r > 0 holds

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ 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 ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

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

n > 0

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 ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) ) )

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ 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 A1, TOPS_1:28;

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 (TOP-REAL n) 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: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then reconsider U = (Ball (x,(2 * (r / 3)))) /\ A as Subset of ((TOP-REAL n) | A) by XBOOLE_1:17;

Ball (x,(2 * (r / 3))) in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

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

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

take U ; :: thesis: ( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

x is Element of REAL n by EUCLID:22;

then A12: |.(x - p).| = |.(p - x).| by EUCLID:18, A5;

|.(x - p).| + (2 * (r / 3)) < (r / 3) + (2 * (r / 3)) by A8, TOPREAL9:7, XREAL_1:6;

then A13: Ball (x,(2 * (r / 3))) c= Ball (p,r) by Th5;

2 * (r / 3) > r / 3 by A6, XREAL_1:155;

then |.(x - p).| < 2 * (r / 3) by A8, TOPREAL9:7, XXREAL_0:2;

then A14: p in Ball (x,(2 * (r / 3))) by A12;

hence p in U by A3, A1, XBOOLE_0:def 4; :: thesis: ( U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ 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 ((TOP-REAL n) | (A \ U)),(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 \ U) = f )

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

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

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

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

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

for r being Real st r > 0 holds

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

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

for r being Real st r > 0 holds

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

set TR = TOP-REAL n;

let p be Point of (TOP-REAL n); :: thesis: ( p in Fr A & A is closed implies for r being Real st r > 0 holds

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ 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 ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

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

n > 0

proof

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
assume
n <= 0
; :: thesis: contradiction

then n = 0 ;

then A4: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by EUCLID:77, EUCLID:22;

[#] (TOP-REAL n) is open ;

hence contradiction by A4, A1, ZFMISC_1:33; :: thesis: verum

end;then n = 0 ;

then A4: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by EUCLID:77, EUCLID:22;

[#] (TOP-REAL n) is open ;

hence contradiction by A4, A1, ZFMISC_1:33; :: thesis: verum

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 ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) ) )

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

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ 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 A1, TOPS_1:28;

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 (TOP-REAL n) 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: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then reconsider U = (Ball (x,(2 * (r / 3)))) /\ A as Subset of ((TOP-REAL n) | A) by XBOOLE_1:17;

Ball (x,(2 * (r / 3))) in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

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

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

take U ; :: thesis: ( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )

x is Element of REAL n by EUCLID:22;

then A12: |.(x - p).| = |.(p - x).| by EUCLID:18, A5;

|.(x - p).| + (2 * (r / 3)) < (r / 3) + (2 * (r / 3)) by A8, TOPREAL9:7, XREAL_1:6;

then A13: Ball (x,(2 * (r / 3))) c= Ball (p,r) by Th5;

2 * (r / 3) > r / 3 by A6, XREAL_1:155;

then |.(x - p).| < 2 * (r / 3) by A8, TOPREAL9:7, XXREAL_0:2;

then A14: p in Ball (x,(2 * (r / 3))) by A12;

hence p in U by A3, A1, XBOOLE_0:def 4; :: thesis: ( U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ 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 ((TOP-REAL n) | (A \ U)),(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 \ U) = f )

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

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

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

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

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

end;

suppose A16:
A \ U is empty
; :: thesis: ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

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

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

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) ;

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;reconsider H = the continuous Function of ((TOP-REAL n) | A),(Tunit_circle (n1 + 1)) as Function of ((TOP-REAL n) | A),(Tunit_circle n) ;

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

suppose A17:
not A \ U is empty
; :: thesis: ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

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

( 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 (TOP-REAL n) by A17;

A18: ( (TOP-REAL n) | AUS is metrizable & (TOP-REAL n) | AUS is finite-ind & (TOP-REAL n) | AUS is second-countable )

then reconsider AU = A \ U, SS = Sphere (x,(2 * (r / 3))) as Subset of ((TOP-REAL n) | AUS) by XBOOLE_1:7;

AU ` = AUS \ AU by SUBSET_1:def 4, A20

.= (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 A6, Th7;

then ind SS = n1 by TOPDIM_1:21;

then A22: ind (AU `) <= n1 by TOPDIM_1:19, A21;

A23: (TOP-REAL n) | (A \ U) = ((TOP-REAL n) | AUS) | AU by A20, PRE_TOPC:7;

then reconsider F = f as Function of (((TOP-REAL n) | AUS) | AU),(Tunit_circle n) ;

A \ U = A \ (Ball (x,(2 * (r / 3)))) by XBOOLE_1:47;

then A24: A \ U is closed by A2, YELLOW_8:20;

then AU is closed by TSEP_1:8;

then consider g being continuous Function of ((TOP-REAL n) | AUS),(Tunit_circle (n1 + 1)) such that

A25: g | AU = F by Th3, A23, A15, A18, A22;

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

then reconsider AclU = A /\ (cl_Ball (x,(2 * (r / 3)))), au = A \ U as Subset of ((TOP-REAL n) | A) by XBOOLE_1:17, XBOOLE_1:36;

set T3 = ((TOP-REAL n) | A) | AclU;

set T4 = ((TOP-REAL n) | A) | au;

A27: (A /\ U) \/ au = A by XBOOLE_1:51;

A ` = ([#] (TOP-REAL n)) \ A by SUBSET_1:def 4;

then not x in A by A7, XBOOLE_0:def 5;

then consider h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (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 A6, Th4;

A30: n1 + 1 = n ;

then A31: dom h = the carrier of ((TOP-REAL n) | A) by A6, FUNCT_2:def 1;

A32: [#] ((TOP-REAL n) | (Sphere (x,(2 * (r / 3))))) = Sphere (x,(2 * (r / 3))) by PRE_TOPC:def 5;

then rng h c= the carrier of (TOP-REAL n) by XBOOLE_1:1;

then reconsider h1 = h as Function of ((TOP-REAL n) | A),(TOP-REAL n) by A31, FUNCT_2:2;

A33: Sphere (x,(2 * (r / 3))) c= AUS by XBOOLE_1:7;

rng h c= [#] ((TOP-REAL n) | (Sphere (x,(2 * (r / 3))))) ;

then reconsider h2 = h1 as Function of ((TOP-REAL n) | A),((TOP-REAL n) | AUS) by A33, A32, XBOOLE_1:1, A31, FUNCT_2:2, A20;

h1 is continuous by A28, PRE_TOPC:26;

then A34: h2 is continuous by PRE_TOPC:27;

set T2 = ((TOP-REAL n) | AUS) | AU;

A35: ((TOP-REAL n) | AUS) | AU = (TOP-REAL n) | (A \ U) by PRE_TOPC:7, XBOOLE_1:7;

A36: (cl_Ball (x,(2 * (r / 3)))) \ (Ball (x,(2 * (r / 3)))) = Sphere (x,(2 * (r / 3))) by JORDAN:19, A9;

A37: (A /\ A) /\ (Ball (x,(2 * (r / 3)))) = A /\ (A /\ (Ball (x,(2 * (r / 3))))) by XBOOLE_1:16;

A38: g | (((TOP-REAL n) | AUS) | AU) = g | the carrier of (((TOP-REAL n) | AUS) | AU) by TMAP_1:def 4;

((TOP-REAL n) | A) | au = (TOP-REAL n) | (A \ U) by XBOOLE_1:36, PRE_TOPC:7;

then reconsider gT2 = g | (((TOP-REAL n) | AUS) | AU) as continuous Function of (((TOP-REAL n) | A) | au),(Tunit_circle (n1 + 1)) by A35, A17;

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

not AclU is empty by A10, A14, A3, A1, XBOOLE_0:def 4;

then reconsider gh2T3 = g * (h2 | (((TOP-REAL n) | A) | AclU)) as continuous Function of (((TOP-REAL n) | A) | AclU),(Tunit_circle (n1 + 1)) by A34;

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

A41: h2 | (((TOP-REAL n) | A) | AclU) = h2 | the carrier of (((TOP-REAL n) | A) | AclU) by A3, A1, TMAP_1:def 4;

au is closed by A24, TSEP_1:8;

then reconsider G = gh2T3 +* gT2 as continuous Function of (((TOP-REAL n) | A) | (AclU \/ au)),(Tunit_circle (n1 + 1)) by A50, A42, PARTFUN1:def 4, TOPGEN_5:10;

W: A /\ (Ball (x,(2 * (r / 3)))) c= AclU by TOPREAL9:16, XBOOLE_1:26;

A = AclU \/ au by A26, W, A27, A37, XBOOLE_1:9;

then A51: ((TOP-REAL n) | A) | (AclU \/ au) = (TOP-REAL n) | A by A26, TSEP_1:93;

then reconsider GG = G as Function of ((TOP-REAL n) | A),(Tunit_circle n) ;

take GG ; :: thesis: ( GG is continuous & GG | (A \ U) = f )

thus GG is continuous by A51; :: thesis: GG | (A \ U) = f

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

A53: dom gT2 = the carrier of (((TOP-REAL n) | A) | au) by FUNCT_2:def 1;

then A56: dom (GG | (A \ U)) = A /\ (A \ U) by RELAT_1:61

.= A \ U by XBOOLE_1:36, XBOOLE_1:28 ;

dom f = A \ U by A30, A52, FUNCT_2:def 1;

hence GG | (A \ U) = f by A54, A56; :: thesis: verum

end;reconsider AUS = (A \ U) \/ (Sphere (x,(2 * (r / 3)))) as non empty Subset of (TOP-REAL n) by A17;

A18: ( (TOP-REAL n) | AUS is metrizable & (TOP-REAL n) | AUS is finite-ind & (TOP-REAL n) | AUS is second-countable )

proof

A20:
[#] ((TOP-REAL n) | AUS) = AUS
by PRE_TOPC:def 5;
reconsider aus = AUS as Subset of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ;

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

(TOP-REAL n) | AUS = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) | aus by PRE_TOPC:36;

hence ( (TOP-REAL n) | AUS is metrizable & (TOP-REAL n) | AUS is finite-ind & (TOP-REAL n) | AUS is second-countable ) by A19; :: thesis: verum

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

(TOP-REAL n) | AUS = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) | aus by PRE_TOPC:36;

hence ( (TOP-REAL n) | AUS is metrizable & (TOP-REAL n) | AUS is finite-ind & (TOP-REAL n) | AUS is second-countable ) by A19; :: thesis: verum

then reconsider AU = A \ U, SS = Sphere (x,(2 * (r / 3))) as Subset of ((TOP-REAL n) | AUS) by XBOOLE_1:7;

AU ` = AUS \ AU by SUBSET_1:def 4, A20

.= (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 A6, Th7;

then ind SS = n1 by TOPDIM_1:21;

then A22: ind (AU `) <= n1 by TOPDIM_1:19, A21;

A23: (TOP-REAL n) | (A \ U) = ((TOP-REAL n) | AUS) | AU by A20, PRE_TOPC:7;

then reconsider F = f as Function of (((TOP-REAL n) | AUS) | AU),(Tunit_circle n) ;

A \ U = A \ (Ball (x,(2 * (r / 3)))) by XBOOLE_1:47;

then A24: A \ U is closed by A2, YELLOW_8:20;

then AU is closed by TSEP_1:8;

then consider g being continuous Function of ((TOP-REAL n) | AUS),(Tunit_circle (n1 + 1)) such that

A25: g | AU = F by Th3, A23, A15, A18, A22;

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

then reconsider AclU = A /\ (cl_Ball (x,(2 * (r / 3)))), au = A \ U as Subset of ((TOP-REAL n) | A) by XBOOLE_1:17, XBOOLE_1:36;

set T3 = ((TOP-REAL n) | A) | AclU;

set T4 = ((TOP-REAL n) | A) | au;

A27: (A /\ U) \/ au = A by XBOOLE_1:51;

A ` = ([#] (TOP-REAL n)) \ A by SUBSET_1:def 4;

then not x in A by A7, XBOOLE_0:def 5;

then consider h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (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 A6, Th4;

A30: n1 + 1 = n ;

then A31: dom h = the carrier of ((TOP-REAL n) | A) by A6, FUNCT_2:def 1;

A32: [#] ((TOP-REAL n) | (Sphere (x,(2 * (r / 3))))) = Sphere (x,(2 * (r / 3))) by PRE_TOPC:def 5;

then rng h c= the carrier of (TOP-REAL n) by XBOOLE_1:1;

then reconsider h1 = h as Function of ((TOP-REAL n) | A),(TOP-REAL n) by A31, FUNCT_2:2;

A33: Sphere (x,(2 * (r / 3))) c= AUS by XBOOLE_1:7;

rng h c= [#] ((TOP-REAL n) | (Sphere (x,(2 * (r / 3))))) ;

then reconsider h2 = h1 as Function of ((TOP-REAL n) | A),((TOP-REAL n) | AUS) by A33, A32, XBOOLE_1:1, A31, FUNCT_2:2, A20;

h1 is continuous by A28, PRE_TOPC:26;

then A34: h2 is continuous by PRE_TOPC:27;

set T2 = ((TOP-REAL n) | AUS) | AU;

A35: ((TOP-REAL n) | AUS) | AU = (TOP-REAL n) | (A \ U) by PRE_TOPC:7, XBOOLE_1:7;

A36: (cl_Ball (x,(2 * (r / 3)))) \ (Ball (x,(2 * (r / 3)))) = Sphere (x,(2 * (r / 3))) by JORDAN:19, A9;

A37: (A /\ A) /\ (Ball (x,(2 * (r / 3)))) = A /\ (A /\ (Ball (x,(2 * (r / 3))))) by XBOOLE_1:16;

A38: g | (((TOP-REAL n) | AUS) | AU) = g | the carrier of (((TOP-REAL n) | AUS) | AU) by TMAP_1:def 4;

((TOP-REAL n) | A) | au = (TOP-REAL n) | (A \ U) by XBOOLE_1:36, PRE_TOPC:7;

then reconsider gT2 = g | (((TOP-REAL n) | AUS) | AU) as continuous Function of (((TOP-REAL n) | A) | au),(Tunit_circle (n1 + 1)) by A35, A17;

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

not AclU is empty by A10, A14, A3, A1, XBOOLE_0:def 4;

then reconsider gh2T3 = g * (h2 | (((TOP-REAL n) | A) | AclU)) as continuous Function of (((TOP-REAL n) | A) | AclU),(Tunit_circle (n1 + 1)) by A34;

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

A41: h2 | (((TOP-REAL n) | A) | AclU) = h2 | the carrier of (((TOP-REAL n) | A) | AclU) by A3, A1, TMAP_1:def 4;

A42: now :: thesis: for x being object st x in (dom gh2T3) /\ (dom gT2) holds

gh2T3 . x = gT2 . x

A50:
AclU is closed
by A2, TSEP_1:8;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 A43, A40, XBOOLE_0:def 5;

x in A by A43, A40, XBOOLE_0:def 5;

then A45: not x in Ball (x,(2 * (r / 3))) by A44, XBOOLE_0:def 4;

A46: x in dom gh2T3 by A43, XBOOLE_0:def 4;

then x in cl_Ball (x,(2 * (r / 3))) by A39, XBOOLE_0:def 4;

then A47: x in Sphere (x,(2 * (r / 3))) by A45, A36, XBOOLE_0:def 5;

A48: x in dom gT2 by A43, XBOOLE_0:def 4;

x in A by A46, A39, XBOOLE_0:def 4;

then A49: x in A /\ (Sphere (x,(2 * (r / 3)))) by A47, XBOOLE_0:def 4;

x in dom (h2 | (((TOP-REAL n) | A) | AclU)) by A46, FUNCT_1:11;

then (h2 | (((TOP-REAL n) | A) | AclU)) . x = h2 . x by A41, FUNCT_1:47

.= (h | (Sphere (x,(2 * (r / 3))))) . x by A47, FUNCT_1:49

.= x by A29, A49, FUNCT_1:17 ;

hence gh2T3 . x = g . x by A46, FUNCT_1:12

.= gT2 . x by A38, A48, FUNCT_1:47 ;

:: thesis: verum

end;assume A43: x in (dom gh2T3) /\ (dom gT2) ; :: thesis: gh2T3 . x = gT2 . x

A44: not x in U by A43, A40, XBOOLE_0:def 5;

x in A by A43, A40, XBOOLE_0:def 5;

then A45: not x in Ball (x,(2 * (r / 3))) by A44, XBOOLE_0:def 4;

A46: x in dom gh2T3 by A43, XBOOLE_0:def 4;

then x in cl_Ball (x,(2 * (r / 3))) by A39, XBOOLE_0:def 4;

then A47: x in Sphere (x,(2 * (r / 3))) by A45, A36, XBOOLE_0:def 5;

A48: x in dom gT2 by A43, XBOOLE_0:def 4;

x in A by A46, A39, XBOOLE_0:def 4;

then A49: x in A /\ (Sphere (x,(2 * (r / 3)))) by A47, XBOOLE_0:def 4;

x in dom (h2 | (((TOP-REAL n) | A) | AclU)) by A46, FUNCT_1:11;

then (h2 | (((TOP-REAL n) | A) | AclU)) . x = h2 . x by A41, FUNCT_1:47

.= (h | (Sphere (x,(2 * (r / 3))))) . x by A47, FUNCT_1:49

.= x by A29, A49, FUNCT_1:17 ;

hence gh2T3 . x = g . x by A46, FUNCT_1:12

.= gT2 . x by A38, A48, FUNCT_1:47 ;

:: thesis: verum

au is closed by A24, TSEP_1:8;

then reconsider G = gh2T3 +* gT2 as continuous Function of (((TOP-REAL n) | A) | (AclU \/ au)),(Tunit_circle (n1 + 1)) by A50, A42, PARTFUN1:def 4, TOPGEN_5:10;

W: A /\ (Ball (x,(2 * (r / 3)))) c= AclU by TOPREAL9:16, XBOOLE_1:26;

A = AclU \/ au by A26, W, A27, A37, XBOOLE_1:9;

then A51: ((TOP-REAL n) | A) | (AclU \/ au) = (TOP-REAL n) | A by A26, TSEP_1:93;

then reconsider GG = G as Function of ((TOP-REAL n) | A),(Tunit_circle n) ;

take GG ; :: thesis: ( GG is continuous & GG | (A \ U) = f )

thus GG is continuous by A51; :: thesis: GG | (A \ U) = f

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

A53: dom gT2 = the carrier of (((TOP-REAL n) | 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

dom GG = A
by A26, FUNCT_2:def 1;(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 A52, FUNCT_1:49

.= gT2 . x by FUNCT_4:13, A55, A52, A40, A53

.= g . x by A38, A40, A52, A53, A55, FUNCT_1:47

.= f . x by A25, A55, A52, FUNCT_1:49 ;

:: thesis: verum

end;assume A55: x in dom f ; :: thesis: (GG | (A \ U)) . x = f . x

hence (GG | (A \ U)) . x = GG . x by A52, FUNCT_1:49

.= gT2 . x by FUNCT_4:13, A55, A52, A40, A53

.= g . x by A38, A40, A52, A53, A55, FUNCT_1:47

.= f . x by A25, A55, A52, FUNCT_1:49 ;

:: thesis: verum

then A56: dom (GG | (A \ U)) = A /\ (A \ U) by RELAT_1:61

.= A \ U by XBOOLE_1:36, XBOOLE_1:28 ;

dom f = A \ U by A30, A52, FUNCT_2:def 1;

hence GG | (A \ U) = f by A54, A56; :: thesis: verum