let n be Nat; :: thesis:
let T be TopSpace; :: thesis:
let A be closed Subset of T; :: thesis:
assume A1: T is normal ; :: thesis:
set TR = TOP-REAL n;
set N = 0. (TOP-REAL n);
set H = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1));
let f be Function of (T | A),((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))); :: thesis:
assume A2: f is continuous ; :: thesis:
A3: [#] ((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by PRE_TOPC:def 5;
A4: [#] (T | A) = A by PRE_TOPC:def 5;

suppose A5: A is empty ; :: thesis:

reconsider TRH = (TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) as non empty TopSpace ;
set g = the continuous Function of T,TRH;
A6: the continuous Function of T,TRH | A = {} by A5;
f = {} by A5;
hence ex g being Function of T,((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) st
( g is continuous & g | A = f ) by A6; :: thesis:

end;

suppose A7: not A is empty ; :: thesis:

set CC = Closed-Interval-TSpace ((- 1),1);

suppose A8: n = 0 ; :: thesis:

reconsider TRH = (TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) as non empty TopSpace ;
A9: {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by EUCLID:22, A8, JORDAN2C:105;
then reconsider Z = 0. (TOP-REAL n) as Point of TRH by A3, ZFMISC_1:33;
ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) = the carrier of (TOP-REAL n) by A9, ZFMISC_1:33;
then A10: rng f = the carrier of (TOP-REAL n) by A4, A7, A3, A9, ZFMISC_1:33;
reconsider g = T --> Z as Function of T,((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) ;
take g ; :: thesis:
A11: the carrier of T /\ A = A by XBOOLE_1:28;
dom f = A by FUNCT_2:def 1, A4;
then f = A --> (0. (TOP-REAL n)) by A10, FUNCOP_1:9, EUCLID:22, A8, JORDAN2C:105;
hence ( g is continuous & g | A = f ) by A11, FUNCOP_1:12; :: thesis:

end;

suppose n <> 0 ; :: thesis:

then reconsider nn = n as non zero Element of NAT by ORDINAL1:def 12;
set CC = Closed-Interval-TSpace ((- 1),1);
reconsider F = f as Function of (T | A),(TOP-REAL n) by FUNCT_2:7, A3;
defpred S₁[ Nat, object ] means ex g being continuous Function of T,R^1 st
( $2 = g & rng g c= [#] (Closed-Interval-TSpace ((- 1),1)) & g | A = (PROJ (n,$1)) * F );
A12: dom f = A by A4, FUNCT_2:def 1;
0. (TOP-REAL n) = 0* n by EUCLID:70;
then A13: 0. (TOP-REAL n) = n |-> 0 by EUCLID:def 4;
A14: for k being Nat st k in Seg n holds
ex x being object st S₁[k,x]

A15: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18;
A16: not T is empty by A7;
let k be Nat; :: thesis:
assume A17: k in Seg n ; :: thesis:
rng f c= ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by A3;
then (PROJ (n,k)) .: (rng F) c= (PROJ (n,k)) .: (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) by RELAT_1:123;
then A18: (PROJ (n,k)) .: (rng F) c= [.(((0. (TOP-REAL n)) . k) - ((n |-> 1) . k)),(((0. (TOP-REAL n)) . k) + ((n |-> 1) . k)).] by A17, Th7;
A19: dom ((PROJ (n,k)) * F) = the carrier of (T | A) by FUNCT_2:def 1;
A20: (0. (TOP-REAL n)) . k = 0 by A13;
(n |-> 1) . k = 1 by A17, FINSEQ_2:57;
then rng ((PROJ (n,k)) * F) c= [.(- 1),1.] by A20, A18, RELAT_1:127;
then reconsider PF = (PROJ (n,k)) * F as Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) by A19, A15, FUNCT_2:2;
A21: F is continuous by A2, PRE_TOPC:26;
PROJ (n,k) is continuous by TOPREALC:57, A17;
then consider g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) such that
A22: g | A = PF by A21, A16, A7, PRE_TOPC:27, A1, TIETZE:23;
A23: rng g c= REAL ;
dom g = the carrier of T by FUNCT_2:def 1;
then reconsider G = g as Function of T,R^1 by A23, TOPMETR:17, FUNCT_2:2;
A24: G is continuous by PRE_TOPC:26;
rng g c= the carrier of (Closed-Interval-TSpace ((- 1),1)) by RELAT_1:def 19;
hence ex x being object st S₁[k,x] by A24, A22; :: thesis:

end;

consider pp being FinSequence such that
A25: dom pp = Seg n and
A26: for k being Nat st k in Seg n holds
S₁[k,pp . k] from FINSEQ_1:sch 1(A14);
A27: len pp = nn by A25, FINSEQ_1:def 3;
rng pp c= Funcs ( the carrier of T, the carrier of R^1)

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng pp ; :: thesis:
then consider k being object such that
A28: k in dom pp and
A29: pp . k = y by FUNCT_1:def 3;
reconsider k = k as Nat by A28;
consider g being continuous Function of T,R^1 such that
A30: pp . k = g and
rng g c= [#] (Closed-Interval-TSpace ((- 1),1)) and
g | A = (PROJ (n,k)) * F by A25, A26, A28;
A31: rng g c= the carrier of R^1 by RELAT_1:def 19;
dom g = the carrier of T by FUNCT_2:def 1;
hence y in Funcs ( the carrier of T, the carrier of R^1) by A31, FUNCT_2:def 2, A29, A30; :: thesis:

end;

then pp is FinSequence of Funcs ( the carrier of T, the carrier of R^1) by FINSEQ_1:def 4;
then reconsider pp = pp as Element of nn -tuples_on (Funcs ( the carrier of T, the carrier of R^1)) by A27, FINSEQ_2:92;
A32: dom <:pp:> = the carrier of T by FUNCT_2:def 1;
A33: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18;
rng <:pp:> c= ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A34: y in rng <:pp:> ; :: thesis:
then consider x being object such that
A35: x in dom <:pp:> and
A36: <:pp:> . x = y by FUNCT_1:def 3;
reconsider p = <:pp:> . x as Point of (TOP-REAL n) by A34, A36;

let j be Nat; :: thesis:
A37: (0. (TOP-REAL n)) . j = 0 by A13;
assume A38: j in Seg n ; :: thesis:
then consider g being continuous Function of T,R^1 such that
A39: g = pp . j and
A40: rng g c= [#] (Closed-Interval-TSpace ((- 1),1)) and
g | A = (PROJ (n,j)) * F by A26;
A41: dom g = the carrier of T by FUNCT_2:def 1;
g . x = p . j by Th20, A39;
then A42: p . j in rng g by A41, A35, FUNCT_1:def 3;
(n |-> 1) . j = 1 by A38, FINSEQ_2:57;
hence p . j in [.(((0. (TOP-REAL n)) . j) - ((n |-> 1) . j)),(((0. (TOP-REAL n)) . j) + ((n |-> 1) . j)).] by A37, A42, A40, A33; :: thesis:

end;

hence y in ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by Def2, A36; :: thesis:

end;

then reconsider G = <:pp:> as Function of T,((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) by A3, A32, FUNCT_2:2;
take G ; :: thesis:
for i being Nat st i in dom pp holds
for h being Function of T,R^1 st h = pp . i holds
h is continuous

let k be Nat; :: thesis:
assume A43: k in dom pp ; :: thesis:
ex g being continuous Function of T,R^1 st
( pp . k = g & rng g c= [#] (Closed-Interval-TSpace ((- 1),1)) & g | A = (PROJ (n,k)) * F ) by A25, A26, A43;
hence for h being Function of T,R^1 st h = pp . k holds
h is continuous ; :: thesis:

end;

hence G is continuous by Th21, PRE_TOPC:27; :: thesis:
A44: dom (G | A) = A by A32, RELAT_1:62;
for e being set st e in dom f holds
(G | A) . e = f . e

let e be set ; :: thesis:
A45: rng F c= the carrier of (TOP-REAL n) ;
assume A46: e in dom f ; :: thesis:
then G . e in rng G by A32, A12, FUNCT_1:def 3;
then A47: G . e in ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by A3;
f . e in rng f by A46, FUNCT_1:def 3;
then reconsider Ge = G . e, fe = f . e as Point of (TOP-REAL n) by A45, A47;
A48: len fe = n by CARD_1:def 7;

A49: now :: thesis:

A50: dom fe = Seg n by A48, FINSEQ_1:def 3;
let w be Nat; :: thesis:
assume that
A51: 1 <= w and
A52: w <= n ; :: thesis:
consider g being continuous Function of T,R^1 such that
A53: g = pp . w and
rng g c= [#] (Closed-Interval-TSpace ((- 1),1)) and
A54: g | A = (PROJ (n,w)) * F by A51, A52, FINSEQ_1:1, A26;
A55: Ge . w = g . e by Th20, A53;
A56: e in dom (g | A) by A46, A12, FUNCT_2:def 1;
(g | A) . e = g . e by A46, A4, FUNCT_1:49;
then Ge . w = (PROJ (n,w)) . fe by A55, A56, A54, FUNCT_1:12;
hence Ge . w = fe /. w by TOPREALC:def 6
.= fe . w by PARTFUN1:def 6, A51, A52, FINSEQ_1:1, A50 ;
:: thesis:

end;

A57: len Ge = n by CARD_1:def 7;
(G | A) . e = G . e by A46, A44, A4, FUNCT_1:47;
hence (G | A) . e = f . e by A49, FINSEQ_1:14, A57, A48; :: thesis:

end;

hence G | A = f by A44, A12; :: thesis:

end;

end;

end;

end;