let n be Nat; :: thesis: for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable holds

for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

defpred S_{1}[ Nat] means for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable holds

for F being closed Subset of TM st ind (F `) <= $1 holds

for f being continuous Function of (TM | F),(Tunit_circle ($1 + 1)) ex g being Function of TM,(Tunit_circle ($1 + 1)) st

( g is continuous & g | F = f );

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f )

assume A1: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

let F be closed Subset of TM; :: thesis: ( ind (F `) <= n implies for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f )

assume A2: ind (F `) <= n ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A160: S_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A160, A3);

then ex g being Function of TM,(Tunit_circle (n + 1)) st

( g is continuous & g | F = f ) by A1, A2;

hence ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f ; :: thesis: verum

for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

defpred S

for F being closed Subset of TM st ind (F `) <= $1 holds

for f being continuous Function of (TM | F),(Tunit_circle ($1 + 1)) ex g being Function of TM,(Tunit_circle ($1 + 1)) st

( g is continuous & g | F = f );

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f )

assume A1: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

let F be closed Subset of TM; :: thesis: ( ind (F `) <= n implies for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f )

assume A2: ind (F `) <= n ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

A3: for n being Nat st S

S

proof

let f be continuous Function of (TM | F),(Tunit_circle (n + 1)); :: thesis: ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set n1 = n + 1;

set n2 = (n + 1) + 1;

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

set Tn1 = TOP-REAL (n + 1);

set Tn2 = TOP-REAL ((n + 1) + 1);

set U = Tunit_circle ((n + 1) + 1);

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= n + 1 holds

for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f ) )

assume A5: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= n + 1 holds

for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

let F be closed Subset of TM; :: thesis: ( ind (F `) <= n + 1 implies for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f ) )

assume A6: ind (F `) <= n + 1 ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

let f be continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)); :: thesis: ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

A7: [#] (TM | F) = F by PRE_TOPC:def 5;

A8: dom f = the carrier of (TM | F) by FUNCT_2:def 1;

A9: dom f = the carrier of (TM | F) by FUNCT_2:def 1;

A10: [#] (TM | F) = F by PRE_TOPC:def 5;

end;set n1 = n + 1;

set n2 = (n + 1) + 1;

assume A4: S

set Tn1 = TOP-REAL (n + 1);

set Tn2 = TOP-REAL ((n + 1) + 1);

set U = Tunit_circle ((n + 1) + 1);

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= n + 1 holds

for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f ) )

assume A5: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= n + 1 holds

for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

let F be closed Subset of TM; :: thesis: ( ind (F `) <= n + 1 implies for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f ) )

assume A6: ind (F `) <= n + 1 ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)) ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

let f be continuous Function of (TM | F),(Tunit_circle ((n + 1) + 1)); :: thesis: ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

A7: [#] (TM | F) = F by PRE_TOPC:def 5;

A8: dom f = the carrier of (TM | F) by FUNCT_2:def 1;

A9: dom f = the carrier of (TM | F) by FUNCT_2:def 1;

A10: [#] (TM | F) = F by PRE_TOPC:def 5;

per cases
( F is empty or not F is empty )
;

end;

suppose A11:
F is empty
; :: thesis: ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

( g is continuous & g | F = f )

take g = TM --> the Point of (Tunit_circle ((n + 1) + 1)); :: thesis: ( g is continuous & g | F = f )

g | F = {} by A11;

hence ( g is continuous & g | F = f ) by A11; :: thesis: verum

end;g | F = {} by A11;

hence ( g is continuous & g | F = f ) by A11; :: thesis: verum

suppose A12:
not F is empty
; :: thesis: ex g being Function of TM,(Tunit_circle ((n + 1) + 1)) st

( g is continuous & g | F = f )

( g is continuous & g | F = f )

set Sn = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } ;

set Sp = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } ;

A13: { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } c= the carrier of (TOP-REAL ((n + 1) + 1))

A14: Sn = { t where t is Point of (TOP-REAL ((n + 1) + 1)) : ( t . ((n + 1) + 1) <= 0 & |.t.| = 1 ) } ;

A15: Sp = { l where l is Point of (TOP-REAL ((n + 1) + 1)) : ( l . ((n + 1) + 1) >= 0 & |.l.| = 1 ) } ;

then reconsider s1 = Sp, s2 = Sn as closed Subset of (TOP-REAL ((n + 1) + 1)) by A14, Th2;

A16: [#] ((TOP-REAL ((n + 1) + 1)) | s2) = s2 by PRE_TOPC:def 5;

Tunit_circle ((n + 1) + 1) = Tcircle ((0. (TOP-REAL ((n + 1) + 1))),1) by TOPREALB:def 7;

then A17: the carrier of (Tunit_circle ((n + 1) + 1)) = Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) by TOPREALB:9;

A18: s1 c= the carrier of (Tunit_circle ((n + 1) + 1))

reconsider A1 = f " S1, A2 = f " S2 as Subset of TM by A7, XBOOLE_1:1;

A24: f .: (A1 /\ A2) c= (f .: A1) /\ (f .: A2) by RELAT_1:121;

A25: f .: A2 c= s2 by FUNCT_1:75;

S1 is closed by TSEP_1:8;

then f " S1 is closed by PRE_TOPC:def 6;

then A26: A1 is closed by A7, TSEP_1:8;

Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) c= S1 \/ S2

then A29: f " (rng f) c= f " (S1 \/ S2) by RELAT_1:143;

f " (rng f) = dom f by RELAT_1:134;

then A30: F = f " (S1 \/ S2) by A29, A7, FUNCT_2:def 1;

then A31: F = A1 \/ A2 by RELAT_1:140;

then reconsider TFA12 = A1 /\ A2 as Subset of (TM | F) by XBOOLE_1:29, A10;

A32: [#] ((TM | F) | TFA12) = TFA12 by PRE_TOPC:def 5;

reconsider fa = f | TFA12 as Function of ((TM | F) | TFA12),((Tunit_circle ((n + 1) + 1)) | (f .: TFA12)) by A10, A12, JORDAN24:12;

A33: fa is continuous by JORDAN24:13, A10, A12;

(dom f) /\ TFA12 = TFA12 by A8, XBOOLE_1:28;

then A34: dom fa = the carrier of ((TM | F) | TFA12) by A32, RELAT_1:61;

A35: (TM | F) | (f " S1) = TM | A1 by PRE_TOPC:7, A7;

then reconsider f1 = f | A1 as Function of (TM | A1),((Tunit_circle ((n + 1) + 1)) | (f .: A1)) by A12, A7, JORDAN24:12;

A36: f1 is continuous by A35, A12, A10, JORDAN24:13;

A37: rng f1 c= the carrier of ((Tunit_circle ((n + 1) + 1)) | (f .: A1)) ;

A38: [#] ((Tunit_circle ((n + 1) + 1)) | (f .: A1)) = f .: A1 by PRE_TOPC:def 5;

then A39: rng f1 c= the carrier of (Tunit_circle ((n + 1) + 1)) by XBOOLE_1:1;

A40: (TM | F) | (f " S2) = TM | A2 by PRE_TOPC:7, A7;

then reconsider f2 = f | A2 as Function of (TM | A2),((Tunit_circle ((n + 1) + 1)) | (f .: A2)) by A12, A7, JORDAN24:12;

A41: f2 is continuous by A40, A12, A10, JORDAN24:13;

A42: [#] ((Tunit_circle ((n + 1) + 1)) | (f .: A2)) = f .: A2 by PRE_TOPC:def 5;

then A43: rng f2 c= the carrier of (Tunit_circle ((n + 1) + 1)) by XBOOLE_1:1;

dom f1 = (dom f) /\ A1 by RELAT_1:61;

then A44: dom f1 = A1 by A9, XBOOLE_1:28;

[#] (TM | A1) = A1 by PRE_TOPC:def 5;

then reconsider f1 = f1 as Function of (TM | A1),(Tunit_circle ((n + 1) + 1)) by A39, FUNCT_2:2, A44;

A45: rng f2 c= the carrier of ((Tunit_circle ((n + 1) + 1)) | (f .: A2)) ;

dom f2 = (dom f) /\ A2 by RELAT_1:61;

then A46: dom f2 = A2 by A9, XBOOLE_1:28;

[#] (TM | A2) = A2 by PRE_TOPC:def 5;

then reconsider f2 = f2 as Function of (TM | A2),(Tunit_circle ((n + 1) + 1)) by A43, A46, FUNCT_2:2;

f .: A2 c= s2 by FUNCT_1:75;

then A47: rng f2 c= s2 by A42, A45;

S2 is closed by TSEP_1:8;

then f " S2 is closed by PRE_TOPC:def 6;

then A48: A2 is closed by A7, TSEP_1:8;

TM | (F `) is second-countable by A5;

then consider X1, X2 being closed Subset of TM such that

A49: [#] TM = X1 \/ X2 and

A50: A1 c= X1 and

A51: A2 c= X2 and

A52: A1 /\ X2 = A1 /\ A2 and

A53: A1 /\ A2 = X1 /\ A2 and

A54: ind ((X1 /\ X2) \ (A1 /\ A2)) <= (n + 1) - 1 by A31, TOPDIM_2:24, A5, A6, A26, A48;

set TX = TM | (X1 /\ X2);

A55: [#] (TM | (X1 /\ X2)) = X1 /\ X2 by PRE_TOPC:def 5;

then reconsider TXA12 = A1 /\ A2 as Subset of (TM | (X1 /\ X2)) by A50, A51, XBOOLE_1:27;

(X1 /\ X2) \ (A1 /\ A2) = TXA12 ` by A55, SUBSET_1:def 4;

then A56: ind (TXA12 `) <= n by A5, TOPDIM_1:21, A54;

set Un = Tunit_circle (n + 1);

set TD = Tdisk ((0. (TOP-REAL (n + 1))),1);

deffunc H_{1}( Nat) -> Element of K10(K11( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)) = PROJ (((n + 1) + 1),$1);

consider FF being FinSequence such that

A57: ( len FF = n + 1 & ( for k being Nat st k in dom FF holds

FF . k = H_{1}(k) ) )
from FINSEQ_1:sch 2();

A58: rng FF c= Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)

then A62: ( cl_Ball ((0. (TOP-REAL (n + 1))),1) is compact & not cl_Ball ((0. (TOP-REAL (n + 1))),1) is boundary & cl_Ball ((0. (TOP-REAL (n + 1))),1) is convex ) ;

reconsider FF = FF as FinSequence of Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) by A58, FINSEQ_1:def 4;

reconsider FF = FF as Element of (n + 1) -tuples_on (Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)) by A57, FINSEQ_2:92;

set FFF = <:FF:>;

A63: s1 /\ s2 c= s2 by XBOOLE_1:17;

A64: <:FF:> .: s2 = cl_Ball ((0. (TOP-REAL (n + 1))),1) by A57, Th1, A15;

then A65: not s2 is empty ;

A66: dom <:FF:> = the carrier of (TOP-REAL ((n + 1) + 1)) by FUNCT_2:def 1;

then s1 /\ (dom <:FF:>) = s1 by XBOOLE_1:28;

then A67: dom (<:FF:> | s1) = s1 by RELAT_1:61;

s2 /\ (dom <:FF:>) = s2 by XBOOLE_1:28, A66;

then A68: dom (<:FF:> | s2) = s2 by RELAT_1:61;

A69: the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) = cl_Ball ((0. (TOP-REAL (n + 1))),1) by BROUWER:3;

then rng (<:FF:> | s2) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by RELAT_1:115, A64;

then reconsider Fs2 = <:FF:> | s2 as Function of ((TOP-REAL ((n + 1) + 1)) | s2),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:2, A16, A68;

A70: [#] ((TOP-REAL ((n + 1) + 1)) | s1) = s1 by PRE_TOPC:def 5;

Fs2 is being_homeomorphism by A57, Th1, A15;

then A71: s2, cl_Ball ((0. (TOP-REAL (n + 1))),1) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

A72: <:FF:> .: s1 = cl_Ball ((0. (TOP-REAL (n + 1))),1) by A57, Th1, A14;

then A73: not s1 is empty ;

rng (<:FF:> | s1) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by RELAT_1:115, A72, A69;

then reconsider Fs1 = <:FF:> | s1 as Function of ((TOP-REAL ((n + 1) + 1)) | s1),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A67, FUNCT_2:2, A70;

A74: Fs1 .: (s1 /\ s2) c= <:FF:> .: (s1 /\ s2) by RELAT_1:128;

A75: Fs1 is being_homeomorphism by A57, Th1, A14;

then A76: rng Fs1 = [#] (Tdisk ((0. (TOP-REAL (n + 1))),1)) by TOPS_2:def 5;

f .: A1 c= s1 by FUNCT_1:75;

then WE: (f .: A1) /\ (f .: A2) c= s1 /\ s2 by A25, XBOOLE_1:27;

then f .: (A1 /\ A2) c= s1 /\ s2 by A24;

then A78: Fs1 .: (f .: (A1 /\ A2)) c= Fs1 .: (s1 /\ s2) by RELAT_1:123;

s1 /\ s2 c= s1 by XBOOLE_1:17;

then A79: f .: (A1 /\ A2) c= s1 by WE, A24;

[#] ((Tunit_circle ((n + 1) + 1)) | (f .: TFA12)) = f .: TFA12 by PRE_TOPC:def 5;

then A80: rng fa c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s1) by A79, A70;

then reconsider fa = fa as Function of ((TM | F) | TFA12),(Tunit_circle ((n + 1) + 1)) by XBOOLE_1:1, A70, A34, FUNCT_2:2;

A81: fa is continuous by A33, PRE_TOPC:26;

rng fa c= the carrier of (TOP-REAL ((n + 1) + 1)) by A17, XBOOLE_1:1;

then reconsider fa = fa as Function of ((TM | F) | TFA12),(TOP-REAL ((n + 1) + 1)) by FUNCT_2:2, A34;

A82: fa is continuous by A81, PRE_TOPC:26;

A83: Fs1 " is continuous by A75, TOPS_2:def 5;

A84: <:FF:> .: (s1 /\ s2) = Sphere ((0. (TOP-REAL (n + 1))),1) by A57, Th1;

then Fs1 .: (s1 /\ s2) = Sphere ((0. (TOP-REAL (n + 1))),1) by XBOOLE_1:17, RELAT_1:129;

then A85: (Fs1 ") .: (Sphere ((0. (TOP-REAL (n + 1))),1)) = Fs1 " (Fs1 .: (s1 /\ s2)) by TOPS_2:55, A75, A76

.= s1 /\ s2 by FUNCT_1:94, A67, A75, XBOOLE_1:17 ;

set A2X = A2 \/ (X1 /\ X2);

set A1X = A1 \/ (X1 /\ X2);

A86: X2 = [#] (TM | X2) by PRE_TOPC:def 5;

(TM | F) | TFA12 = TM | (A1 /\ A2) by PRE_TOPC:7, A31, XBOOLE_1:29;

then A87: (TM | F) | TFA12 = (TM | (X1 /\ X2)) | TXA12 by PRE_TOPC:7, A50, A51, XBOOLE_1:27;

then reconsider fa = fa as Function of ((TM | (X1 /\ X2)) | TXA12),((TOP-REAL ((n + 1) + 1)) | s1) by A34, FUNCT_2:2, A80;

reconsider Ffa = Fs1 * fa as Function of ((TM | (X1 /\ X2)) | TXA12),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A73;

A88: [#] ((TM | (X1 /\ X2)) | TXA12) = TXA12 by PRE_TOPC:def 5;

then A89: dom Ffa = A1 /\ A2 by FUNCT_2:def 1;

rng Ffa = Ffa .: (dom Ffa) by RELAT_1:113

.= (Fs1 * fa) .: (A1 /\ A2) by A88, FUNCT_2:def 1

.= Fs1 .: (fa .: (A1 /\ A2)) by RELAT_1:126 ;

then E: rng Ffa c= Fs1 .: (f .: (A1 /\ A2)) by RELAT_1:123, RELAT_1:128;

then A90: rng Ffa c= Fs1 .: (s1 /\ s2) by A78;

A91: rng Ffa c= Sphere ((0. (TOP-REAL (n + 1))),1) by E, A78, A74, A84;

fa is continuous by A82, PRE_TOPC:27, A87;

then A92: Ffa is continuous by TOPS_2:46, A75, A73;

reconsider Ffa = Ffa as Function of ((TM | (X1 /\ X2)) | TXA12),(TOP-REAL (n + 1)) by A91, XBOOLE_1:1, FUNCT_2:2, A89, A88;

Tunit_circle (n + 1) = Tcircle ((0. (TOP-REAL (n + 1))),1) by TOPREALB:def 7;

then A93: the carrier of (Tunit_circle (n + 1)) = Sphere ((0. (TOP-REAL (n + 1))),1) by TOPREALB:9;

then reconsider H = Ffa as Function of ((TM | (X1 /\ X2)) | TXA12),(Tunit_circle (n + 1)) by FUNCT_2:2, A89, A88, A90, A74, XBOOLE_1:1, A84;

Ffa is continuous by A92, PRE_TOPC:26;

then reconsider H = H as continuous Function of ((TM | (X1 /\ X2)) | TXA12),(Tunit_circle (n + 1)) by PRE_TOPC:27;

TXA12 is closed by A26, A48, TSEP_1:8;

then consider g being Function of (TM | (X1 /\ X2)),(Tunit_circle (n + 1)) such that

A94: g is continuous and

A95: g | TXA12 = H by A5, A56, A4;

A96: rng g c= the carrier of (TOP-REAL (n + 1)) by A93, XBOOLE_1:1;

A97: dom g = the carrier of (TM | (X1 /\ X2)) by FUNCT_2:def 1;

A98: rng g c= the carrier of (Tunit_circle (n + 1)) ;

reconsider g = g as Function of (TM | (X1 /\ X2)),(TOP-REAL (n + 1)) by A97, A96, FUNCT_2:2;

A99: g is continuous by A94, PRE_TOPC:26;

the carrier of (Tunit_circle (n + 1)) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by A93, A69, TOPREAL9:17;

then reconsider g = g as Function of (TM | (X1 /\ X2)),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A98, XBOOLE_1:1, FUNCT_2:2, A97;

reconsider G = (Fs1 ") * g as Function of (TM | (X1 /\ X2)),((TOP-REAL ((n + 1) + 1)) | s1) ;

A100: dom G = the carrier of (TM | (X1 /\ X2)) by FUNCT_2:def 1, A73;

g is continuous by A99, PRE_TOPC:27;

then A101: G is continuous by A83, TOPS_2:46;

A102: rng G c= s1 by A70;

then reconsider G = G as Function of (TM | (X1 /\ X2)),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A100;

A103: G is continuous by PRE_TOPC:26, A101;

reconsider G = G as Function of (TM | (X1 /\ X2)),(Tunit_circle ((n + 1) + 1)) by A18, A102, XBOOLE_1:1, FUNCT_2:2, A100;

A104: G is continuous by PRE_TOPC:27, A103;

A105: rng fa c= dom Fs1 by A67, A70;

A106: G | TXA12 = (Fs1 ") * (g | TXA12) by RELAT_1:83

.= ((Fs1 ") * Fs1) * fa by RELAT_1:36, A95

.= (id (dom Fs1)) * fa by TOPS_2:52, A75, A76

.= fa by RELAT_1:53, A105 ;

.= (Fs1 ") .: (g .: (dom G)) by RELAT_1:126

.= (Fs1 ") .: (rng g) by A97, A100, RELAT_1:113 ;

then rng G c= s1 /\ s2 by A85, A93, A98, RELAT_1:123;

then rng G c= s2 by A63;

then A115: (rng f2) \/ (rng G) c= s2 by XBOOLE_1:8, A47;

f2 is continuous by A41, PRE_TOPC:26;

then reconsider f2G = f2 +* G as continuous Function of (TM | (A2 \/ (X1 /\ X2))),(Tunit_circle ((n + 1) + 1)) by A111, PARTFUN1:def 4, A104, A48, TOPGEN_5:10;

A116: dom f2G = the carrier of (TM | (A2 \/ (X1 /\ X2))) by FUNCT_2:def 1;

A117: rng f2G c= (rng f2) \/ (rng G) by FUNCT_4:17;

then rng f2G c= s2 by A115;

then reconsider f2G = f2G as Function of (TM | (A2 \/ (X1 /\ X2))),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A116;

A118: f2G is continuous by PRE_TOPC:26;

reconsider f2G = f2G as Function of (TM | (A2 \/ (X1 /\ X2))),((TOP-REAL ((n + 1) + 1)) | s2) by FUNCT_2:2, A116, A115, A117, XBOOLE_1:1, A16;

( cl_Ball ((0. (TOP-REAL (n + 1))),1) is compact & not cl_Ball ((0. (TOP-REAL (n + 1))),1) is boundary & cl_Ball ((0. (TOP-REAL (n + 1))),1) is convex ) by A61;

then consider H2 being Function of TM,((TOP-REAL ((n + 1) + 1)) | s2) such that

A119: H2 is continuous and

A120: H2 | (A2 \/ (X1 /\ X2)) = f2G by A118, PRE_TOPC:27, A71, TIETZE_2:24, A48;

A121: not TM is empty by A12;

then reconsider H2X = H2 | X2 as Function of (TM | X2),(((TOP-REAL ((n + 1) + 1)) | s2) | (H2 .: X2)) by JORDAN24:12, A65;

A122: H2X is continuous by JORDAN24:13, A65, A121, A119;

dom H2 = the carrier of TM by FUNCT_2:def 1, A65;

then A123: dom H2X = X2 /\ the carrier of TM by RELAT_1:61;

then A124: dom H2X = the carrier of (TM | X2) by XBOOLE_1:28, A86;

f1 is continuous by A36, PRE_TOPC:26;

then reconsider f1G = f1 +* G as continuous Function of (TM | (A1 \/ (X1 /\ X2))),(Tunit_circle ((n + 1) + 1)) by A107, PARTFUN1:def 4, A104, A26, TOPGEN_5:10;

A125: dom f1G = the carrier of (TM | (A1 \/ (X1 /\ X2))) by FUNCT_2:def 1;

f .: A1 c= s1 by FUNCT_1:75;

then rng f1 c= s1 by A38, A37;

then A126: (rng f1) \/ (rng G) c= s1 by A102, XBOOLE_1:8;

A127: rng f1G c= (rng f1) \/ (rng G) by FUNCT_4:17;

then rng f1G c= s1 by A126;

then reconsider f1G = f1G as Function of (TM | (A1 \/ (X1 /\ X2))),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A125;

A128: f1G is continuous by PRE_TOPC:26;

reconsider f1G = f1G as Function of (TM | (A1 \/ (X1 /\ X2))),((TOP-REAL ((n + 1) + 1)) | s1) by FUNCT_2:2, A125, A126, A127, XBOOLE_1:1, A70;

s1, cl_Ball ((0. (TOP-REAL (n + 1))),1) are_homeomorphic by T_0TOPSP:def 1, A75, METRIZTS:def 1;

then consider H1 being Function of TM,((TOP-REAL ((n + 1) + 1)) | s1) such that

A129: H1 is continuous and

A130: H1 | (A1 \/ (X1 /\ X2)) = f1G by A62, A26, A128, PRE_TOPC:27, TIETZE_2:24;

reconsider H1X = H1 | X1 as Function of (TM | X1),(((TOP-REAL ((n + 1) + 1)) | s1) | (H1 .: X1)) by A121, JORDAN24:12, A73;

A131: H1X is continuous by JORDAN24:13, A73, A121, A129;

[#] (((TOP-REAL ((n + 1) + 1)) | s1) | (H1 .: X1)) = H1 .: X1 by PRE_TOPC:def 5;

then A132: rng H1X c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s1) by XBOOLE_1:1;

dom H1 = the carrier of TM by FUNCT_2:def 1, A73;

then A133: dom H1X = X1 /\ the carrier of TM by RELAT_1:61;

then A134: dom H1X = X1 by XBOOLE_1:28;

X1 = [#] (TM | X1) by PRE_TOPC:def 5;

then A135: dom H1X = the carrier of (TM | X1) by A133, XBOOLE_1:28;

then reconsider H1X = H1X as Function of (TM | X1),((TOP-REAL ((n + 1) + 1)) | s1) by A132, FUNCT_2:2;

A136: H1X is continuous by A131, PRE_TOPC:26;

A137: rng H1X c= s1 by A70;

[#] (((TOP-REAL ((n + 1) + 1)) | s2) | (H2 .: X2)) = H2 .: X2 by PRE_TOPC:def 5;

then rng H2X c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s2) by XBOOLE_1:1;

then reconsider H2X = H2X as Function of (TM | X2),((TOP-REAL ((n + 1) + 1)) | s2) by A124, FUNCT_2:2;

A138: H2X is continuous by A122, PRE_TOPC:26;

reconsider H1X = H1X as Function of (TM | X1),(TOP-REAL ((n + 1) + 1)) by A137, XBOOLE_1:1, A135, FUNCT_2:2;

A139: rng H2X c= s2 by A16;

then reconsider H2X = H2X as Function of (TM | X2),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, A124, FUNCT_2:2;

A140: H2X is continuous by A138, PRE_TOPC:26;

then reconsider H12 = H1X +* H2X as continuous Function of (TM | (X1 \/ X2)),(TOP-REAL ((n + 1) + 1)) by A140, A141, PARTFUN1:def 4, TOPGEN_5:10;

A149: TM | (X1 \/ X2) = TopStruct(# the carrier of TM, the topology of TM #) by A49, TSEP_1:93;

then reconsider H12 = H12 as Function of TM,(TOP-REAL ((n + 1) + 1)) ;

A150: rng H12 c= (rng H1X) \/ (rng H2X) by FUNCT_4:17;

F /\ X1 = (A1 \/ A2) /\ X1 by A30, RELAT_1:140

.= (A1 /\ X1) \/ (A2 /\ X1) by XBOOLE_1:23

.= A1 \/ (A2 /\ X1) by A50, XBOOLE_1:28

.= A1 by A53, XBOOLE_1:17, XBOOLE_1:12 ;

then A151: H1X | F = H1 | A1 by RELAT_1:71;

f1G = G +* f1 by A107, PARTFUN1:def 4, FUNCT_4:34;

then A152: f1G | A1 = f1 by FUNCT_4:23, A44;

A153: F /\ X2 = (A1 \/ A2) /\ X2 by A30, RELAT_1:140

.= (A1 /\ X2) \/ (A2 /\ X2) by XBOOLE_1:23

.= (A1 /\ X2) \/ A2 by A51, XBOOLE_1:28

.= A2 by A52, XBOOLE_1:17, XBOOLE_1:12 ;

A154: H2 | A2 = f2G | A2 by A120, RELAT_1:74, XBOOLE_1:7;

(rng H1X) \/ (rng H2X) c= s1 \/ s2 by A139, A137, XBOOLE_1:13;

then A155: rng H12 c= s1 \/ s2 by A150;

A156: dom H12 = the carrier of TM by FUNCT_2:def 1;

A157: H12 is continuous by PRE_TOPC:32, A149;

s1 \/ s2 c= Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) by A18, A21, A17, XBOOLE_1:8;

then reconsider H12 = H12 as Function of TM,(Tunit_circle ((n + 1) + 1)) by A155, XBOOLE_1:1, A17, A156, FUNCT_2:2;

take H12 ; :: thesis: ( H12 is continuous & H12 | F = f )

thus H12 is continuous by PRE_TOPC:27, A157; :: thesis: H12 | F = f

A158: H1 | A1 = f1G | A1 by A130, XBOOLE_1:7, RELAT_1:74;

f2G = G +* f2 by A111, PARTFUN1:def 4, FUNCT_4:34;

then A159: f2G | A2 = f2 by FUNCT_4:23, A46;

thus H12 | F = (H1X | F) +* (H2X | F) by FUNCT_4:71

.= f1 +* f2 by A152, A159, A158, A154, A151, RELAT_1:71, A153

.= f | (A1 \/ A2) by FUNCT_4:78

.= f by A31, A10 ; :: thesis: verum

end;set Sp = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } ;

A13: { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } c= the carrier of (TOP-REAL ((n + 1) + 1))

proof

{ p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } c= the carrier of (TOP-REAL ((n + 1) + 1))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } or x in the carrier of (TOP-REAL ((n + 1) + 1)) )

assume x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL ((n + 1) + 1))

then ex p being Point of (TOP-REAL ((n + 1) + 1)) st

( p = x & p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) ;

hence x in the carrier of (TOP-REAL ((n + 1) + 1)) ; :: thesis: verum

end;assume x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL ((n + 1) + 1))

then ex p being Point of (TOP-REAL ((n + 1) + 1)) st

( p = x & p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) ;

hence x in the carrier of (TOP-REAL ((n + 1) + 1)) ; :: thesis: verum

proof

then reconsider Sp = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) >= 0 & |.p.| = 1 ) } , Sn = { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } as Subset of (TOP-REAL ((n + 1) + 1)) by A13;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } or x in the carrier of (TOP-REAL ((n + 1) + 1)) )

assume x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL ((n + 1) + 1))

then ex p being Point of (TOP-REAL ((n + 1) + 1)) st

( p = x & p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) ;

hence x in the carrier of (TOP-REAL ((n + 1) + 1)) ; :: thesis: verum

end;assume x in { p where p is Point of (TOP-REAL ((n + 1) + 1)) : ( p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL ((n + 1) + 1))

then ex p being Point of (TOP-REAL ((n + 1) + 1)) st

( p = x & p . ((n + 1) + 1) <= 0 & |.p.| = 1 ) ;

hence x in the carrier of (TOP-REAL ((n + 1) + 1)) ; :: thesis: verum

A14: Sn = { t where t is Point of (TOP-REAL ((n + 1) + 1)) : ( t . ((n + 1) + 1) <= 0 & |.t.| = 1 ) } ;

A15: Sp = { l where l is Point of (TOP-REAL ((n + 1) + 1)) : ( l . ((n + 1) + 1) >= 0 & |.l.| = 1 ) } ;

then reconsider s1 = Sp, s2 = Sn as closed Subset of (TOP-REAL ((n + 1) + 1)) by A14, Th2;

A16: [#] ((TOP-REAL ((n + 1) + 1)) | s2) = s2 by PRE_TOPC:def 5;

Tunit_circle ((n + 1) + 1) = Tcircle ((0. (TOP-REAL ((n + 1) + 1))),1) by TOPREALB:def 7;

then A17: the carrier of (Tunit_circle ((n + 1) + 1)) = Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) by TOPREALB:9;

A18: s1 c= the carrier of (Tunit_circle ((n + 1) + 1))

proof

A21:
s2 c= the carrier of (Tunit_circle ((n + 1) + 1))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s1 or x in the carrier of (Tunit_circle ((n + 1) + 1)) )

assume x in s1 ; :: thesis: x in the carrier of (Tunit_circle ((n + 1) + 1))

then consider p being Point of (TOP-REAL ((n + 1) + 1)) such that

A19: x = p and

p . ((n + 1) + 1) >= 0 and

A20: |.p.| = 1 ;

p - (0. (TOP-REAL ((n + 1) + 1))) = p by RLVECT_1:13;

hence x in the carrier of (Tunit_circle ((n + 1) + 1)) by A20, A19, A17; :: thesis: verum

end;assume x in s1 ; :: thesis: x in the carrier of (Tunit_circle ((n + 1) + 1))

then consider p being Point of (TOP-REAL ((n + 1) + 1)) such that

A19: x = p and

p . ((n + 1) + 1) >= 0 and

A20: |.p.| = 1 ;

p - (0. (TOP-REAL ((n + 1) + 1))) = p by RLVECT_1:13;

hence x in the carrier of (Tunit_circle ((n + 1) + 1)) by A20, A19, A17; :: thesis: verum

proof

then reconsider S1 = s1, S2 = s2 as Subset of (Tunit_circle ((n + 1) + 1)) by A18;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s2 or x in the carrier of (Tunit_circle ((n + 1) + 1)) )

assume x in s2 ; :: thesis: x in the carrier of (Tunit_circle ((n + 1) + 1))

then consider p being Point of (TOP-REAL ((n + 1) + 1)) such that

A22: x = p and

p . ((n + 1) + 1) <= 0 and

A23: |.p.| = 1 ;

p - (0. (TOP-REAL ((n + 1) + 1))) = p by RLVECT_1:13;

hence x in the carrier of (Tunit_circle ((n + 1) + 1)) by A23, A22, A17; :: thesis: verum

end;assume x in s2 ; :: thesis: x in the carrier of (Tunit_circle ((n + 1) + 1))

then consider p being Point of (TOP-REAL ((n + 1) + 1)) such that

A22: x = p and

p . ((n + 1) + 1) <= 0 and

A23: |.p.| = 1 ;

p - (0. (TOP-REAL ((n + 1) + 1))) = p by RLVECT_1:13;

hence x in the carrier of (Tunit_circle ((n + 1) + 1)) by A23, A22, A17; :: thesis: verum

reconsider A1 = f " S1, A2 = f " S2 as Subset of TM by A7, XBOOLE_1:1;

A24: f .: (A1 /\ A2) c= (f .: A1) /\ (f .: A2) by RELAT_1:121;

A25: f .: A2 c= s2 by FUNCT_1:75;

S1 is closed by TSEP_1:8;

then f " S1 is closed by PRE_TOPC:def 6;

then A26: A1 is closed by A7, TSEP_1:8;

Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) c= S1 \/ S2

proof

then
rng f c= S1 \/ S2
by A17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) or x in S1 \/ S2 )

assume A27: x in Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) ; :: thesis: x in S1 \/ S2

then reconsider p = x as Point of (TOP-REAL ((n + 1) + 1)) ;

A28: ( p . ((n + 1) + 1) >= 0 or p . ((n + 1) + 1) <= 0 ) ;

|.p.| = 1 by A27, TOPREAL9:12;

then ( p in Sp or p in Sn ) by A28;

hence x in S1 \/ S2 by XBOOLE_0:def 3; :: thesis: verum

end;assume A27: x in Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) ; :: thesis: x in S1 \/ S2

then reconsider p = x as Point of (TOP-REAL ((n + 1) + 1)) ;

A28: ( p . ((n + 1) + 1) >= 0 or p . ((n + 1) + 1) <= 0 ) ;

|.p.| = 1 by A27, TOPREAL9:12;

then ( p in Sp or p in Sn ) by A28;

hence x in S1 \/ S2 by XBOOLE_0:def 3; :: thesis: verum

then A29: f " (rng f) c= f " (S1 \/ S2) by RELAT_1:143;

f " (rng f) = dom f by RELAT_1:134;

then A30: F = f " (S1 \/ S2) by A29, A7, FUNCT_2:def 1;

then A31: F = A1 \/ A2 by RELAT_1:140;

then reconsider TFA12 = A1 /\ A2 as Subset of (TM | F) by XBOOLE_1:29, A10;

A32: [#] ((TM | F) | TFA12) = TFA12 by PRE_TOPC:def 5;

reconsider fa = f | TFA12 as Function of ((TM | F) | TFA12),((Tunit_circle ((n + 1) + 1)) | (f .: TFA12)) by A10, A12, JORDAN24:12;

A33: fa is continuous by JORDAN24:13, A10, A12;

(dom f) /\ TFA12 = TFA12 by A8, XBOOLE_1:28;

then A34: dom fa = the carrier of ((TM | F) | TFA12) by A32, RELAT_1:61;

A35: (TM | F) | (f " S1) = TM | A1 by PRE_TOPC:7, A7;

then reconsider f1 = f | A1 as Function of (TM | A1),((Tunit_circle ((n + 1) + 1)) | (f .: A1)) by A12, A7, JORDAN24:12;

A36: f1 is continuous by A35, A12, A10, JORDAN24:13;

A37: rng f1 c= the carrier of ((Tunit_circle ((n + 1) + 1)) | (f .: A1)) ;

A38: [#] ((Tunit_circle ((n + 1) + 1)) | (f .: A1)) = f .: A1 by PRE_TOPC:def 5;

then A39: rng f1 c= the carrier of (Tunit_circle ((n + 1) + 1)) by XBOOLE_1:1;

A40: (TM | F) | (f " S2) = TM | A2 by PRE_TOPC:7, A7;

then reconsider f2 = f | A2 as Function of (TM | A2),((Tunit_circle ((n + 1) + 1)) | (f .: A2)) by A12, A7, JORDAN24:12;

A41: f2 is continuous by A40, A12, A10, JORDAN24:13;

A42: [#] ((Tunit_circle ((n + 1) + 1)) | (f .: A2)) = f .: A2 by PRE_TOPC:def 5;

then A43: rng f2 c= the carrier of (Tunit_circle ((n + 1) + 1)) by XBOOLE_1:1;

dom f1 = (dom f) /\ A1 by RELAT_1:61;

then A44: dom f1 = A1 by A9, XBOOLE_1:28;

[#] (TM | A1) = A1 by PRE_TOPC:def 5;

then reconsider f1 = f1 as Function of (TM | A1),(Tunit_circle ((n + 1) + 1)) by A39, FUNCT_2:2, A44;

A45: rng f2 c= the carrier of ((Tunit_circle ((n + 1) + 1)) | (f .: A2)) ;

dom f2 = (dom f) /\ A2 by RELAT_1:61;

then A46: dom f2 = A2 by A9, XBOOLE_1:28;

[#] (TM | A2) = A2 by PRE_TOPC:def 5;

then reconsider f2 = f2 as Function of (TM | A2),(Tunit_circle ((n + 1) + 1)) by A43, A46, FUNCT_2:2;

f .: A2 c= s2 by FUNCT_1:75;

then A47: rng f2 c= s2 by A42, A45;

S2 is closed by TSEP_1:8;

then f " S2 is closed by PRE_TOPC:def 6;

then A48: A2 is closed by A7, TSEP_1:8;

TM | (F `) is second-countable by A5;

then consider X1, X2 being closed Subset of TM such that

A49: [#] TM = X1 \/ X2 and

A50: A1 c= X1 and

A51: A2 c= X2 and

A52: A1 /\ X2 = A1 /\ A2 and

A53: A1 /\ A2 = X1 /\ A2 and

A54: ind ((X1 /\ X2) \ (A1 /\ A2)) <= (n + 1) - 1 by A31, TOPDIM_2:24, A5, A6, A26, A48;

set TX = TM | (X1 /\ X2);

A55: [#] (TM | (X1 /\ X2)) = X1 /\ X2 by PRE_TOPC:def 5;

then reconsider TXA12 = A1 /\ A2 as Subset of (TM | (X1 /\ X2)) by A50, A51, XBOOLE_1:27;

(X1 /\ X2) \ (A1 /\ A2) = TXA12 ` by A55, SUBSET_1:def 4;

then A56: ind (TXA12 `) <= n by A5, TOPDIM_1:21, A54;

set Un = Tunit_circle (n + 1);

set TD = Tdisk ((0. (TOP-REAL (n + 1))),1);

deffunc H

consider FF being FinSequence such that

A57: ( len FF = n + 1 & ( for k being Nat st k in dom FF holds

FF . k = H

A58: rng FF c= Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)

proof

A61:
Ball ((0. (TOP-REAL (n + 1))),1) c= Int (cl_Ball ((0. (TOP-REAL (n + 1))),1))
by TOPREAL9:16, TOPS_1:24;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng FF or x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) )

assume x in rng FF ; :: thesis: x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)

then consider i being object such that

A59: i in dom FF and

A60: FF . i = x by FUNCT_1:def 3;

reconsider i = i as Nat by A59;

H_{1}(i) in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)
by FUNCT_2:8;

hence x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) by A57, A59, A60; :: thesis: verum

end;assume x in rng FF ; :: thesis: x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)

then consider i being object such that

A59: i in dom FF and

A60: FF . i = x by FUNCT_1:def 3;

reconsider i = i as Nat by A59;

H

hence x in Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) by A57, A59, A60; :: thesis: verum

then A62: ( cl_Ball ((0. (TOP-REAL (n + 1))),1) is compact & not cl_Ball ((0. (TOP-REAL (n + 1))),1) is boundary & cl_Ball ((0. (TOP-REAL (n + 1))),1) is convex ) ;

reconsider FF = FF as FinSequence of Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1) by A58, FINSEQ_1:def 4;

reconsider FF = FF as Element of (n + 1) -tuples_on (Funcs ( the carrier of (TOP-REAL ((n + 1) + 1)), the carrier of R^1)) by A57, FINSEQ_2:92;

set FFF = <:FF:>;

A63: s1 /\ s2 c= s2 by XBOOLE_1:17;

A64: <:FF:> .: s2 = cl_Ball ((0. (TOP-REAL (n + 1))),1) by A57, Th1, A15;

then A65: not s2 is empty ;

A66: dom <:FF:> = the carrier of (TOP-REAL ((n + 1) + 1)) by FUNCT_2:def 1;

then s1 /\ (dom <:FF:>) = s1 by XBOOLE_1:28;

then A67: dom (<:FF:> | s1) = s1 by RELAT_1:61;

s2 /\ (dom <:FF:>) = s2 by XBOOLE_1:28, A66;

then A68: dom (<:FF:> | s2) = s2 by RELAT_1:61;

A69: the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) = cl_Ball ((0. (TOP-REAL (n + 1))),1) by BROUWER:3;

then rng (<:FF:> | s2) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by RELAT_1:115, A64;

then reconsider Fs2 = <:FF:> | s2 as Function of ((TOP-REAL ((n + 1) + 1)) | s2),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:2, A16, A68;

A70: [#] ((TOP-REAL ((n + 1) + 1)) | s1) = s1 by PRE_TOPC:def 5;

Fs2 is being_homeomorphism by A57, Th1, A15;

then A71: s2, cl_Ball ((0. (TOP-REAL (n + 1))),1) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

A72: <:FF:> .: s1 = cl_Ball ((0. (TOP-REAL (n + 1))),1) by A57, Th1, A14;

then A73: not s1 is empty ;

rng (<:FF:> | s1) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by RELAT_1:115, A72, A69;

then reconsider Fs1 = <:FF:> | s1 as Function of ((TOP-REAL ((n + 1) + 1)) | s1),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A67, FUNCT_2:2, A70;

A74: Fs1 .: (s1 /\ s2) c= <:FF:> .: (s1 /\ s2) by RELAT_1:128;

A75: Fs1 is being_homeomorphism by A57, Th1, A14;

then A76: rng Fs1 = [#] (Tdisk ((0. (TOP-REAL (n + 1))),1)) by TOPS_2:def 5;

f .: A1 c= s1 by FUNCT_1:75;

then WE: (f .: A1) /\ (f .: A2) c= s1 /\ s2 by A25, XBOOLE_1:27;

then f .: (A1 /\ A2) c= s1 /\ s2 by A24;

then A78: Fs1 .: (f .: (A1 /\ A2)) c= Fs1 .: (s1 /\ s2) by RELAT_1:123;

s1 /\ s2 c= s1 by XBOOLE_1:17;

then A79: f .: (A1 /\ A2) c= s1 by WE, A24;

[#] ((Tunit_circle ((n + 1) + 1)) | (f .: TFA12)) = f .: TFA12 by PRE_TOPC:def 5;

then A80: rng fa c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s1) by A79, A70;

then reconsider fa = fa as Function of ((TM | F) | TFA12),(Tunit_circle ((n + 1) + 1)) by XBOOLE_1:1, A70, A34, FUNCT_2:2;

A81: fa is continuous by A33, PRE_TOPC:26;

rng fa c= the carrier of (TOP-REAL ((n + 1) + 1)) by A17, XBOOLE_1:1;

then reconsider fa = fa as Function of ((TM | F) | TFA12),(TOP-REAL ((n + 1) + 1)) by FUNCT_2:2, A34;

A82: fa is continuous by A81, PRE_TOPC:26;

A83: Fs1 " is continuous by A75, TOPS_2:def 5;

A84: <:FF:> .: (s1 /\ s2) = Sphere ((0. (TOP-REAL (n + 1))),1) by A57, Th1;

then Fs1 .: (s1 /\ s2) = Sphere ((0. (TOP-REAL (n + 1))),1) by XBOOLE_1:17, RELAT_1:129;

then A85: (Fs1 ") .: (Sphere ((0. (TOP-REAL (n + 1))),1)) = Fs1 " (Fs1 .: (s1 /\ s2)) by TOPS_2:55, A75, A76

.= s1 /\ s2 by FUNCT_1:94, A67, A75, XBOOLE_1:17 ;

set A2X = A2 \/ (X1 /\ X2);

set A1X = A1 \/ (X1 /\ X2);

A86: X2 = [#] (TM | X2) by PRE_TOPC:def 5;

(TM | F) | TFA12 = TM | (A1 /\ A2) by PRE_TOPC:7, A31, XBOOLE_1:29;

then A87: (TM | F) | TFA12 = (TM | (X1 /\ X2)) | TXA12 by PRE_TOPC:7, A50, A51, XBOOLE_1:27;

then reconsider fa = fa as Function of ((TM | (X1 /\ X2)) | TXA12),((TOP-REAL ((n + 1) + 1)) | s1) by A34, FUNCT_2:2, A80;

reconsider Ffa = Fs1 * fa as Function of ((TM | (X1 /\ X2)) | TXA12),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A73;

A88: [#] ((TM | (X1 /\ X2)) | TXA12) = TXA12 by PRE_TOPC:def 5;

then A89: dom Ffa = A1 /\ A2 by FUNCT_2:def 1;

rng Ffa = Ffa .: (dom Ffa) by RELAT_1:113

.= (Fs1 * fa) .: (A1 /\ A2) by A88, FUNCT_2:def 1

.= Fs1 .: (fa .: (A1 /\ A2)) by RELAT_1:126 ;

then E: rng Ffa c= Fs1 .: (f .: (A1 /\ A2)) by RELAT_1:123, RELAT_1:128;

then A90: rng Ffa c= Fs1 .: (s1 /\ s2) by A78;

A91: rng Ffa c= Sphere ((0. (TOP-REAL (n + 1))),1) by E, A78, A74, A84;

fa is continuous by A82, PRE_TOPC:27, A87;

then A92: Ffa is continuous by TOPS_2:46, A75, A73;

reconsider Ffa = Ffa as Function of ((TM | (X1 /\ X2)) | TXA12),(TOP-REAL (n + 1)) by A91, XBOOLE_1:1, FUNCT_2:2, A89, A88;

Tunit_circle (n + 1) = Tcircle ((0. (TOP-REAL (n + 1))),1) by TOPREALB:def 7;

then A93: the carrier of (Tunit_circle (n + 1)) = Sphere ((0. (TOP-REAL (n + 1))),1) by TOPREALB:9;

then reconsider H = Ffa as Function of ((TM | (X1 /\ X2)) | TXA12),(Tunit_circle (n + 1)) by FUNCT_2:2, A89, A88, A90, A74, XBOOLE_1:1, A84;

Ffa is continuous by A92, PRE_TOPC:26;

then reconsider H = H as continuous Function of ((TM | (X1 /\ X2)) | TXA12),(Tunit_circle (n + 1)) by PRE_TOPC:27;

TXA12 is closed by A26, A48, TSEP_1:8;

then consider g being Function of (TM | (X1 /\ X2)),(Tunit_circle (n + 1)) such that

A94: g is continuous and

A95: g | TXA12 = H by A5, A56, A4;

A96: rng g c= the carrier of (TOP-REAL (n + 1)) by A93, XBOOLE_1:1;

A97: dom g = the carrier of (TM | (X1 /\ X2)) by FUNCT_2:def 1;

A98: rng g c= the carrier of (Tunit_circle (n + 1)) ;

reconsider g = g as Function of (TM | (X1 /\ X2)),(TOP-REAL (n + 1)) by A97, A96, FUNCT_2:2;

A99: g is continuous by A94, PRE_TOPC:26;

the carrier of (Tunit_circle (n + 1)) c= the carrier of (Tdisk ((0. (TOP-REAL (n + 1))),1)) by A93, A69, TOPREAL9:17;

then reconsider g = g as Function of (TM | (X1 /\ X2)),(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A98, XBOOLE_1:1, FUNCT_2:2, A97;

reconsider G = (Fs1 ") * g as Function of (TM | (X1 /\ X2)),((TOP-REAL ((n + 1) + 1)) | s1) ;

A100: dom G = the carrier of (TM | (X1 /\ X2)) by FUNCT_2:def 1, A73;

g is continuous by A99, PRE_TOPC:27;

then A101: G is continuous by A83, TOPS_2:46;

A102: rng G c= s1 by A70;

then reconsider G = G as Function of (TM | (X1 /\ X2)),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A100;

A103: G is continuous by PRE_TOPC:26, A101;

reconsider G = G as Function of (TM | (X1 /\ X2)),(Tunit_circle ((n + 1) + 1)) by A18, A102, XBOOLE_1:1, FUNCT_2:2, A100;

A104: G is continuous by PRE_TOPC:27, A103;

A105: rng fa c= dom Fs1 by A67, A70;

A106: G | TXA12 = (Fs1 ") * (g | TXA12) by RELAT_1:83

.= ((Fs1 ") * Fs1) * fa by RELAT_1:36, A95

.= (id (dom Fs1)) * fa by TOPS_2:52, A75, A76

.= fa by RELAT_1:53, A105 ;

A107: now :: thesis: for xx being object st xx in (dom f1) /\ (dom G) holds

G . xx = f1 . xx

G . xx = f1 . xx

let xx be object ; :: thesis: ( xx in (dom f1) /\ (dom G) implies G . xx = f1 . xx )

assume A108: xx in (dom f1) /\ (dom G) ; :: thesis: G . xx = f1 . xx

then A109: xx in A1 by A44, XBOOLE_0:def 4;

xx in X2 by A108, A55, XBOOLE_0:def 4;

then A110: xx in A1 /\ A2 by A109, A52, XBOOLE_0:def 4;

hence G . xx = (G | TXA12) . xx by FUNCT_1:49

.= f . xx by A110, FUNCT_1:49, A106

.= f1 . xx by A109, FUNCT_1:49 ;

:: thesis: verum

end;assume A108: xx in (dom f1) /\ (dom G) ; :: thesis: G . xx = f1 . xx

then A109: xx in A1 by A44, XBOOLE_0:def 4;

xx in X2 by A108, A55, XBOOLE_0:def 4;

then A110: xx in A1 /\ A2 by A109, A52, XBOOLE_0:def 4;

hence G . xx = (G | TXA12) . xx by FUNCT_1:49

.= f . xx by A110, FUNCT_1:49, A106

.= f1 . xx by A109, FUNCT_1:49 ;

:: thesis: verum

A111: now :: thesis: for xx being object st xx in (dom f2) /\ (dom G) holds

G . xx = f2 . xx

rng G =
G .: (dom G)
by RELAT_1:113
G . xx = f2 . xx

let xx be object ; :: thesis: ( xx in (dom f2) /\ (dom G) implies G . xx = f2 . xx )

assume A112: xx in (dom f2) /\ (dom G) ; :: thesis: G . xx = f2 . xx

then A113: xx in A2 by A46, XBOOLE_0:def 4;

xx in X1 by A112, A55, XBOOLE_0:def 4;

then A114: xx in A1 /\ A2 by A113, A53, XBOOLE_0:def 4;

hence G . xx = (G | TXA12) . xx by FUNCT_1:49

.= f . xx by A114, FUNCT_1:49, A106

.= f2 . xx by A113, FUNCT_1:49 ;

:: thesis: verum

end;assume A112: xx in (dom f2) /\ (dom G) ; :: thesis: G . xx = f2 . xx

then A113: xx in A2 by A46, XBOOLE_0:def 4;

xx in X1 by A112, A55, XBOOLE_0:def 4;

then A114: xx in A1 /\ A2 by A113, A53, XBOOLE_0:def 4;

hence G . xx = (G | TXA12) . xx by FUNCT_1:49

.= f . xx by A114, FUNCT_1:49, A106

.= f2 . xx by A113, FUNCT_1:49 ;

:: thesis: verum

.= (Fs1 ") .: (g .: (dom G)) by RELAT_1:126

.= (Fs1 ") .: (rng g) by A97, A100, RELAT_1:113 ;

then rng G c= s1 /\ s2 by A85, A93, A98, RELAT_1:123;

then rng G c= s2 by A63;

then A115: (rng f2) \/ (rng G) c= s2 by XBOOLE_1:8, A47;

f2 is continuous by A41, PRE_TOPC:26;

then reconsider f2G = f2 +* G as continuous Function of (TM | (A2 \/ (X1 /\ X2))),(Tunit_circle ((n + 1) + 1)) by A111, PARTFUN1:def 4, A104, A48, TOPGEN_5:10;

A116: dom f2G = the carrier of (TM | (A2 \/ (X1 /\ X2))) by FUNCT_2:def 1;

A117: rng f2G c= (rng f2) \/ (rng G) by FUNCT_4:17;

then rng f2G c= s2 by A115;

then reconsider f2G = f2G as Function of (TM | (A2 \/ (X1 /\ X2))),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A116;

A118: f2G is continuous by PRE_TOPC:26;

reconsider f2G = f2G as Function of (TM | (A2 \/ (X1 /\ X2))),((TOP-REAL ((n + 1) + 1)) | s2) by FUNCT_2:2, A116, A115, A117, XBOOLE_1:1, A16;

( cl_Ball ((0. (TOP-REAL (n + 1))),1) is compact & not cl_Ball ((0. (TOP-REAL (n + 1))),1) is boundary & cl_Ball ((0. (TOP-REAL (n + 1))),1) is convex ) by A61;

then consider H2 being Function of TM,((TOP-REAL ((n + 1) + 1)) | s2) such that

A119: H2 is continuous and

A120: H2 | (A2 \/ (X1 /\ X2)) = f2G by A118, PRE_TOPC:27, A71, TIETZE_2:24, A48;

A121: not TM is empty by A12;

then reconsider H2X = H2 | X2 as Function of (TM | X2),(((TOP-REAL ((n + 1) + 1)) | s2) | (H2 .: X2)) by JORDAN24:12, A65;

A122: H2X is continuous by JORDAN24:13, A65, A121, A119;

dom H2 = the carrier of TM by FUNCT_2:def 1, A65;

then A123: dom H2X = X2 /\ the carrier of TM by RELAT_1:61;

then A124: dom H2X = the carrier of (TM | X2) by XBOOLE_1:28, A86;

f1 is continuous by A36, PRE_TOPC:26;

then reconsider f1G = f1 +* G as continuous Function of (TM | (A1 \/ (X1 /\ X2))),(Tunit_circle ((n + 1) + 1)) by A107, PARTFUN1:def 4, A104, A26, TOPGEN_5:10;

A125: dom f1G = the carrier of (TM | (A1 \/ (X1 /\ X2))) by FUNCT_2:def 1;

f .: A1 c= s1 by FUNCT_1:75;

then rng f1 c= s1 by A38, A37;

then A126: (rng f1) \/ (rng G) c= s1 by A102, XBOOLE_1:8;

A127: rng f1G c= (rng f1) \/ (rng G) by FUNCT_4:17;

then rng f1G c= s1 by A126;

then reconsider f1G = f1G as Function of (TM | (A1 \/ (X1 /\ X2))),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, FUNCT_2:2, A125;

A128: f1G is continuous by PRE_TOPC:26;

reconsider f1G = f1G as Function of (TM | (A1 \/ (X1 /\ X2))),((TOP-REAL ((n + 1) + 1)) | s1) by FUNCT_2:2, A125, A126, A127, XBOOLE_1:1, A70;

s1, cl_Ball ((0. (TOP-REAL (n + 1))),1) are_homeomorphic by T_0TOPSP:def 1, A75, METRIZTS:def 1;

then consider H1 being Function of TM,((TOP-REAL ((n + 1) + 1)) | s1) such that

A129: H1 is continuous and

A130: H1 | (A1 \/ (X1 /\ X2)) = f1G by A62, A26, A128, PRE_TOPC:27, TIETZE_2:24;

reconsider H1X = H1 | X1 as Function of (TM | X1),(((TOP-REAL ((n + 1) + 1)) | s1) | (H1 .: X1)) by A121, JORDAN24:12, A73;

A131: H1X is continuous by JORDAN24:13, A73, A121, A129;

[#] (((TOP-REAL ((n + 1) + 1)) | s1) | (H1 .: X1)) = H1 .: X1 by PRE_TOPC:def 5;

then A132: rng H1X c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s1) by XBOOLE_1:1;

dom H1 = the carrier of TM by FUNCT_2:def 1, A73;

then A133: dom H1X = X1 /\ the carrier of TM by RELAT_1:61;

then A134: dom H1X = X1 by XBOOLE_1:28;

X1 = [#] (TM | X1) by PRE_TOPC:def 5;

then A135: dom H1X = the carrier of (TM | X1) by A133, XBOOLE_1:28;

then reconsider H1X = H1X as Function of (TM | X1),((TOP-REAL ((n + 1) + 1)) | s1) by A132, FUNCT_2:2;

A136: H1X is continuous by A131, PRE_TOPC:26;

A137: rng H1X c= s1 by A70;

[#] (((TOP-REAL ((n + 1) + 1)) | s2) | (H2 .: X2)) = H2 .: X2 by PRE_TOPC:def 5;

then rng H2X c= the carrier of ((TOP-REAL ((n + 1) + 1)) | s2) by XBOOLE_1:1;

then reconsider H2X = H2X as Function of (TM | X2),((TOP-REAL ((n + 1) + 1)) | s2) by A124, FUNCT_2:2;

A138: H2X is continuous by A122, PRE_TOPC:26;

reconsider H1X = H1X as Function of (TM | X1),(TOP-REAL ((n + 1) + 1)) by A137, XBOOLE_1:1, A135, FUNCT_2:2;

A139: rng H2X c= s2 by A16;

then reconsider H2X = H2X as Function of (TM | X2),(TOP-REAL ((n + 1) + 1)) by XBOOLE_1:1, A124, FUNCT_2:2;

A140: H2X is continuous by A138, PRE_TOPC:26;

A141: now :: thesis: for xx being object st xx in (dom H1X) /\ (dom H2X) holds

H1X . xx = H2X . xx

H1X is continuous
by A136, PRE_TOPC:26;H1X . xx = H2X . xx

let xx be object ; :: thesis: ( xx in (dom H1X) /\ (dom H2X) implies H1X . xx = H2X . xx )

assume A142: xx in (dom H1X) /\ (dom H2X) ; :: thesis: H1X . xx = H2X . xx

then A143: H2X . xx = H2 . xx by A86, FUNCT_1:49;

xx in X1 by A142, A134, XBOOLE_0:def 4;

then A144: H1X . xx = H1 . xx by FUNCT_1:49;

A145: xx in X1 /\ X2 by A142, A123, XBOOLE_1:28, A134;

then A146: xx in A2 \/ (X1 /\ X2) by XBOOLE_0:def 3;

xx in A1 \/ (X1 /\ X2) by A145, XBOOLE_0:def 3;

then A147: H1 . xx = (H1 | (A1 \/ (X1 /\ X2))) . xx by FUNCT_1:49;

A148: f2G . xx = G . xx by A145, A100, A55, FUNCT_4:13;

f1G . xx = G . xx by A145, A100, A55, FUNCT_4:13;

hence H1X . xx = H2X . xx by A148, A147, A146, FUNCT_1:49, A144, A143, A120, A130; :: thesis: verum

end;assume A142: xx in (dom H1X) /\ (dom H2X) ; :: thesis: H1X . xx = H2X . xx

then A143: H2X . xx = H2 . xx by A86, FUNCT_1:49;

xx in X1 by A142, A134, XBOOLE_0:def 4;

then A144: H1X . xx = H1 . xx by FUNCT_1:49;

A145: xx in X1 /\ X2 by A142, A123, XBOOLE_1:28, A134;

then A146: xx in A2 \/ (X1 /\ X2) by XBOOLE_0:def 3;

xx in A1 \/ (X1 /\ X2) by A145, XBOOLE_0:def 3;

then A147: H1 . xx = (H1 | (A1 \/ (X1 /\ X2))) . xx by FUNCT_1:49;

A148: f2G . xx = G . xx by A145, A100, A55, FUNCT_4:13;

f1G . xx = G . xx by A145, A100, A55, FUNCT_4:13;

hence H1X . xx = H2X . xx by A148, A147, A146, FUNCT_1:49, A144, A143, A120, A130; :: thesis: verum

then reconsider H12 = H1X +* H2X as continuous Function of (TM | (X1 \/ X2)),(TOP-REAL ((n + 1) + 1)) by A140, A141, PARTFUN1:def 4, TOPGEN_5:10;

A149: TM | (X1 \/ X2) = TopStruct(# the carrier of TM, the topology of TM #) by A49, TSEP_1:93;

then reconsider H12 = H12 as Function of TM,(TOP-REAL ((n + 1) + 1)) ;

A150: rng H12 c= (rng H1X) \/ (rng H2X) by FUNCT_4:17;

F /\ X1 = (A1 \/ A2) /\ X1 by A30, RELAT_1:140

.= (A1 /\ X1) \/ (A2 /\ X1) by XBOOLE_1:23

.= A1 \/ (A2 /\ X1) by A50, XBOOLE_1:28

.= A1 by A53, XBOOLE_1:17, XBOOLE_1:12 ;

then A151: H1X | F = H1 | A1 by RELAT_1:71;

f1G = G +* f1 by A107, PARTFUN1:def 4, FUNCT_4:34;

then A152: f1G | A1 = f1 by FUNCT_4:23, A44;

A153: F /\ X2 = (A1 \/ A2) /\ X2 by A30, RELAT_1:140

.= (A1 /\ X2) \/ (A2 /\ X2) by XBOOLE_1:23

.= (A1 /\ X2) \/ A2 by A51, XBOOLE_1:28

.= A2 by A52, XBOOLE_1:17, XBOOLE_1:12 ;

A154: H2 | A2 = f2G | A2 by A120, RELAT_1:74, XBOOLE_1:7;

(rng H1X) \/ (rng H2X) c= s1 \/ s2 by A139, A137, XBOOLE_1:13;

then A155: rng H12 c= s1 \/ s2 by A150;

A156: dom H12 = the carrier of TM by FUNCT_2:def 1;

A157: H12 is continuous by PRE_TOPC:32, A149;

s1 \/ s2 c= Sphere ((0. (TOP-REAL ((n + 1) + 1))),1) by A18, A21, A17, XBOOLE_1:8;

then reconsider H12 = H12 as Function of TM,(Tunit_circle ((n + 1) + 1)) by A155, XBOOLE_1:1, A17, A156, FUNCT_2:2;

take H12 ; :: thesis: ( H12 is continuous & H12 | F = f )

thus H12 is continuous by PRE_TOPC:27, A157; :: thesis: H12 | F = f

A158: H1 | A1 = f1G | A1 by A130, XBOOLE_1:7, RELAT_1:74;

f2G = G +* f2 by A111, PARTFUN1:def 4, FUNCT_4:34;

then A159: f2G | A2 = f2 by FUNCT_4:23, A46;

thus H12 | F = (H1X | F) +* (H2X | F) by FUNCT_4:71

.= f1 +* f2 by A152, A159, A158, A154, A151, RELAT_1:71, A153

.= f | (A1 \/ A2) by FUNCT_4:78

.= f by A31, A10 ; :: thesis: verum

A160: S

proof

for n being Nat holds S
reconsider Z = 0 as Real ;

set TR = TOP-REAL 1;

set U = Tunit_circle (0 + 1);

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= 0 holds

for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f ) )

assume A161: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= 0 holds

for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f )

let F be closed Subset of TM; :: thesis: ( ind (F `) <= 0 implies for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f ) )

assume A162: ind (F `) <= 0 ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f )

let f be continuous Function of (TM | F),(Tunit_circle (0 + 1)); :: thesis: ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f )

A164: f " (rng f) = f " the carrier of (Tunit_circle (0 + 1)) by RELAT_1:143, RELAT_1:135;

Tunit_circle (0 + 1) = Tcircle ((0. (TOP-REAL 1)),1) by TOPREALB:def 7;

then A165: the carrier of (Tunit_circle (0 + 1)) = Sphere ((0. (TOP-REAL 1)),1) by TOPREALB:9;

0. (TOP-REAL 1) = 0* (0 + 1) by EUCLID:70

.= <*0*> by FINSEQ_2:59 ;

then A166: {<*(Z - 1)*>,<*(Z + 1)*>} = Fr (Ball ((0. (TOP-REAL 1)),1)) by TOPDIM_2:18;

A167: Fr (Ball ((0. (TOP-REAL 1)),1)) = Sphere ((0. (TOP-REAL 1)),1) by JORDAN:24;

then reconsider mONE = <*(- 1)*>, ONE = <*1*> as Point of (Tunit_circle (0 + 1)) by A165, TARSKI:def 2, A166;

reconsider Q = {ONE}, Q1 = {mONE} as closed Subset of (Tunit_circle (0 + 1)) ;

set F1 = f " Q;

set F2 = f " Q1;

A168: [#] (TM | F) = F by PRE_TOPC:def 5;

then reconsider A1 = f " Q, A2 = f " Q1 as Subset of TM by XBOOLE_1:1;

A169: dom f = F by A168, FUNCT_2:def 1;

Q \/ Q1 = the carrier of (Tunit_circle (0 + 1)) by A166, A167, A165, ENUMSET1:1;

then A170: (f " Q) \/ (f " Q1) = f " the carrier of (Tunit_circle (0 + 1)) by RELAT_1:140

.= F by A164, RELAT_1:134, A169 ;

f " Q1 is closed by PRE_TOPC:def 6;

then A171: A2 is closed by TSEP_1:8, A168;

f " Q is closed by PRE_TOPC:def 6;

then A172: A1 is closed by TSEP_1:8, A168;

ONE <> mONE

TM | (F `) is second-countable by A161;

then consider X1, X2 being closed Subset of TM such that

A174: [#] TM = X1 \/ X2 and

A175: A1 c= X1 and

A176: A2 c= X2 and

( A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 ) and

A177: ind ((X1 /\ X2) \ (A1 /\ A2)) <= 0 - 1 by A161, A162, A170, TOPDIM_2:24, A172, A171;

ind (X1 /\ X2) >= - 1 by TOPDIM_1:5, A161;

then A178: X1 /\ X2 is empty by A177, W, XXREAL_0:1, TOPDIM_1:6, A161;

set h1 = (TM | X1) --> ONE;

set h2 = (TM | X2) --> mONE;

A179: [#] (TM | X1) = X1 by PRE_TOPC:def 5;

A180: dom ((TM | X2) --> mONE) = the carrier of (TM | X2) ;

A181: [#] (TM | X2) = X2 by PRE_TOPC:def 5;

dom ((TM | X1) --> ONE) = the carrier of (TM | X1) ;

then (TM | X1) --> ONE tolerates (TM | X2) --> mONE by A178, A179, A180, A181, XBOOLE_0:def 7, PARTFUN1:56;

then reconsider h12 = ((TM | X1) --> ONE) +* ((TM | X2) --> mONE) as continuous Function of (TM | ([#] TM)),(Tunit_circle (0 + 1)) by A174, TOPGEN_5:10;

[#] (TM | ([#] TM)) = [#] TM by PRE_TOPC:def 5;

then reconsider H12 = h12 as Function of TM,(Tunit_circle (0 + 1)) ;

A182: for x being object st x in F holds

(H12 | F) . x = f . x

TM | ([#] TM) = TopStruct(# the carrier of TM, the topology of TM #) by TSEP_1:93;

hence H12 is continuous by PRE_TOPC:32; :: thesis: H12 | F = f

dom H12 = the carrier of TM by FUNCT_2:def 1;

then dom (H12 | F) = F by RELAT_1:62;

hence H12 | F = f by A182, A168, FUNCT_2:def 1; :: thesis: verum

end;set TR = TOP-REAL 1;

set U = Tunit_circle (0 + 1);

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable implies for F being closed Subset of TM st ind (F `) <= 0 holds

for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f ) )

assume A161: ( TM is finite-ind & TM is second-countable ) ; :: thesis: for F being closed Subset of TM st ind (F `) <= 0 holds

for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f )

let F be closed Subset of TM; :: thesis: ( ind (F `) <= 0 implies for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f ) )

assume A162: ind (F `) <= 0 ; :: thesis: for f being continuous Function of (TM | F),(Tunit_circle (0 + 1)) ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f )

let f be continuous Function of (TM | F),(Tunit_circle (0 + 1)); :: thesis: ex g being Function of TM,(Tunit_circle (0 + 1)) st

( g is continuous & g | F = f )

A164: f " (rng f) = f " the carrier of (Tunit_circle (0 + 1)) by RELAT_1:143, RELAT_1:135;

Tunit_circle (0 + 1) = Tcircle ((0. (TOP-REAL 1)),1) by TOPREALB:def 7;

then A165: the carrier of (Tunit_circle (0 + 1)) = Sphere ((0. (TOP-REAL 1)),1) by TOPREALB:9;

0. (TOP-REAL 1) = 0* (0 + 1) by EUCLID:70

.= <*0*> by FINSEQ_2:59 ;

then A166: {<*(Z - 1)*>,<*(Z + 1)*>} = Fr (Ball ((0. (TOP-REAL 1)),1)) by TOPDIM_2:18;

A167: Fr (Ball ((0. (TOP-REAL 1)),1)) = Sphere ((0. (TOP-REAL 1)),1) by JORDAN:24;

then reconsider mONE = <*(- 1)*>, ONE = <*1*> as Point of (Tunit_circle (0 + 1)) by A165, TARSKI:def 2, A166;

reconsider Q = {ONE}, Q1 = {mONE} as closed Subset of (Tunit_circle (0 + 1)) ;

set F1 = f " Q;

set F2 = f " Q1;

A168: [#] (TM | F) = F by PRE_TOPC:def 5;

then reconsider A1 = f " Q, A2 = f " Q1 as Subset of TM by XBOOLE_1:1;

A169: dom f = F by A168, FUNCT_2:def 1;

Q \/ Q1 = the carrier of (Tunit_circle (0 + 1)) by A166, A167, A165, ENUMSET1:1;

then A170: (f " Q) \/ (f " Q1) = f " the carrier of (Tunit_circle (0 + 1)) by RELAT_1:140

.= F by A164, RELAT_1:134, A169 ;

f " Q1 is closed by PRE_TOPC:def 6;

then A171: A2 is closed by TSEP_1:8, A168;

f " Q is closed by PRE_TOPC:def 6;

then A172: A1 is closed by TSEP_1:8, A168;

ONE <> mONE

proof

then W:
f " Q misses f " Q1
by ZFMISC_1:11, FUNCT_1:71;
assume
ONE = mONE
; :: thesis: contradiction

then <*1*> . 1 = - 1 by FINSEQ_1:40;

hence contradiction ; :: thesis: verum

end;then <*1*> . 1 = - 1 by FINSEQ_1:40;

hence contradiction ; :: thesis: verum

TM | (F `) is second-countable by A161;

then consider X1, X2 being closed Subset of TM such that

A174: [#] TM = X1 \/ X2 and

A175: A1 c= X1 and

A176: A2 c= X2 and

( A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 ) and

A177: ind ((X1 /\ X2) \ (A1 /\ A2)) <= 0 - 1 by A161, A162, A170, TOPDIM_2:24, A172, A171;

ind (X1 /\ X2) >= - 1 by TOPDIM_1:5, A161;

then A178: X1 /\ X2 is empty by A177, W, XXREAL_0:1, TOPDIM_1:6, A161;

set h1 = (TM | X1) --> ONE;

set h2 = (TM | X2) --> mONE;

A179: [#] (TM | X1) = X1 by PRE_TOPC:def 5;

A180: dom ((TM | X2) --> mONE) = the carrier of (TM | X2) ;

A181: [#] (TM | X2) = X2 by PRE_TOPC:def 5;

dom ((TM | X1) --> ONE) = the carrier of (TM | X1) ;

then (TM | X1) --> ONE tolerates (TM | X2) --> mONE by A178, A179, A180, A181, XBOOLE_0:def 7, PARTFUN1:56;

then reconsider h12 = ((TM | X1) --> ONE) +* ((TM | X2) --> mONE) as continuous Function of (TM | ([#] TM)),(Tunit_circle (0 + 1)) by A174, TOPGEN_5:10;

[#] (TM | ([#] TM)) = [#] TM by PRE_TOPC:def 5;

then reconsider H12 = h12 as Function of TM,(Tunit_circle (0 + 1)) ;

A182: for x being object st x in F holds

(H12 | F) . x = f . x

proof

take
H12
; :: thesis: ( H12 is continuous & H12 | F = f )
let x be object ; :: thesis: ( x in F implies (H12 | F) . x = f . x )

assume A183: x in F ; :: thesis: (H12 | F) . x = f . x

then A184: (H12 | F) . x = h12 . x by FUNCT_1:49;

end;assume A183: x in F ; :: thesis: (H12 | F) . x = f . x

then A184: (H12 | F) . x = h12 . x by FUNCT_1:49;

per cases
( x in f " Q or x in f " Q1 )
by A183, A170, XBOOLE_0:def 3;

end;

suppose A185:
x in f " Q
; :: thesis: (H12 | F) . x = f . x

then
not x in dom ((TM | X2) --> mONE)
by A175, A178, XBOOLE_0:def 4, A181;

then A186: H12 . x = ((TM | X1) --> ONE) . x by FUNCT_4:11;

A187: f . x in {ONE} by A185, FUNCT_1:def 7;

((TM | X1) --> ONE) . x = ONE by A185, A175, A179, FUNCOP_1:7;

hence (H12 | F) . x = f . x by A187, TARSKI:def 1, A186, A184; :: thesis: verum

end;then A186: H12 . x = ((TM | X1) --> ONE) . x by FUNCT_4:11;

A187: f . x in {ONE} by A185, FUNCT_1:def 7;

((TM | X1) --> ONE) . x = ONE by A185, A175, A179, FUNCOP_1:7;

hence (H12 | F) . x = f . x by A187, TARSKI:def 1, A186, A184; :: thesis: verum

suppose A188:
x in f " Q1
; :: thesis: (H12 | F) . x = f . x

then A189:
f . x in {mONE}
by FUNCT_1:def 7;

A190: ((TM | X2) --> mONE) . x = mONE by A188, A176, A181, FUNCOP_1:7;

H12 . x = ((TM | X2) --> mONE) . x by A188, A176, A180, A181, FUNCT_4:13;

hence (H12 | F) . x = f . x by A189, TARSKI:def 1, A190, A184; :: thesis: verum

end;A190: ((TM | X2) --> mONE) . x = mONE by A188, A176, A181, FUNCOP_1:7;

H12 . x = ((TM | X2) --> mONE) . x by A188, A176, A180, A181, FUNCT_4:13;

hence (H12 | F) . x = f . x by A189, TARSKI:def 1, A190, A184; :: thesis: verum

TM | ([#] TM) = TopStruct(# the carrier of TM, the topology of TM #) by TSEP_1:93;

hence H12 is continuous by PRE_TOPC:32; :: thesis: H12 | F = f

dom H12 = the carrier of TM by FUNCT_2:def 1;

then dom (H12 | F) = F by RELAT_1:62;

hence H12 | F = f by A182, A168, FUNCT_2:def 1; :: thesis: verum

then ex g being Function of TM,(Tunit_circle (n + 1)) st

( g is continuous & g | F = f ) by A1, A2;

hence ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f ; :: thesis: verum