let T be non empty TopSpace; :: thesis:
assume A1: T is normal ; :: thesis:
let A be closed Subset of T; :: thesis:
let f be Function of (T | A),(Closed-Interval-TSpace ((- 1),1)); :: thesis:
assume A2: f is continuous ; :: thesis:
A3: the carrier of (T | A) = A by PRE_TOPC:8;
A4: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18;

per cases ;

suppose A is empty ; :: thesis:

then reconsider A1 = A as empty Subset of T ;
set g = T --> (R^1 0);
T --> (R^1 0) = the carrier of T --> 0 by TOPREALB:def 2;
then A5: rng (T --> (R^1 0)) = {0} by FUNCOP_1:8;
rng (T --> (R^1 0)) c= the carrier of (Closed-Interval-TSpace ((- 1),1))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (T --> (R^1 0)) ; :: thesis:
then y = 0 by A5, TARSKI:def 1;
hence y in the carrier of (Closed-Interval-TSpace ((- 1),1)) by A4, XXREAL_1:1; :: thesis:

end;

then reconsider g = T --> (R^1 0) as Function of T,(Closed-Interval-TSpace ((- 1),1)) by FUNCT_2:6;
reconsider g = g as continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) by PRE_TOPC:27;
take g ; :: thesis:
g | A1 is empty ;
hence g | A = f ; :: thesis:

end;

suppose not A is empty ; :: thesis:

then reconsider A1 = A as non empty Subset of T ;
set DF = Funcs ( the carrier of T, the carrier of R^1);
set D = { q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } ;
reconsider f1 = f as Function of (T | A1),R^1 by TOPREALA:7;
defpred S₁[ Element of NAT , set , set ] means ex E2 being continuous Function of T,R^1 st
( E2 = $2 & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ $1) implies ex g being continuous Function of T,R^1 st
( $3 = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ($1 + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ($1 + 1)) ) ) );
A6: 2 / 3 > 0 ;
f1 is continuous by A2, PRE_TOPC:26;
then reconsider f1 = f as continuous Function of (T | A1),R^1 ;
T --> (R^1 0) is Element of Funcs ( the carrier of T, the carrier of R^1) by FUNCT_2:8;
then T --> (R^1 0) in { q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } ;
then reconsider D = { q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } as non empty set ;
f1,A is_absolutely_bounded_by 1

proof

let x be set ; :: according to TIETZE:def 1 :: thesis:
assume x in A /\ (dom f1) ; :: thesis:
then x in dom f1 by XBOOLE_0:def 4;
then A7: f1 . x in rng f1 by FUNCT_1:def 3;
rng f1 c= the carrier of (Closed-Interval-TSpace ((- 1),1)) by RELAT_1:def 19;
then ( - 1 <= f1 . x & f1 . x <= 1 ) by A4, A7, XXREAL_1:1;
hence abs (f1 . x) <= 1 by ABSVALUE:5; :: thesis:

end;

then consider g0 being continuous Function of T,R^1 such that
A8: g0, dom g0 is_absolutely_bounded_by 1 / 3 and
A9: f1 - g0,A is_absolutely_bounded_by (2 * 1) / 3 by A1, Th19;
g0 in Funcs ( the carrier of T, the carrier of R^1) by FUNCT_2:8;
then g0 in D ;
then reconsider g0d = g0 as Element of D ;
A10: for n being Element of NAT
for x being Element of D ex y being Element of D st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis:
let x be Element of D; :: thesis:
x in D ;
then consider E2 being Element of Funcs ( the carrier of T, the carrier of R^1) such that
A11: E2 = x and
A12: E2 is continuous Function of T,R^1 ;
reconsider E2 = E2 as continuous Function of T,R^1 by A12;

per cases ;

suppose A13: not f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; :: thesis:

take x ; :: thesis:
take E2 ; :: thesis:
thus ( E2 = x & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st
( x = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) ) by A11, A13; :: thesis:

end;

suppose A14: f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; :: thesis:

reconsider E2b = E2 | A as Function of (T | A1),R^1 by PRE_TOPC:9;
reconsider E2b = E2b as continuous Function of (T | A1),R^1 by TOPMETR:7;
E2b c= E2 by RELAT_1:59;
then A15: f - E2b,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) by A14, Th4, Th17;
set r = (2 / 3) * ((2 / 3) |^ n);
reconsider f1c = f1, E2c = E2b as continuous RealMap of (T | A1) by TOPMETR:17, TOPREAL6:74;
set k = f1 - E2b;
reconsider E2a = E2 as RealMap of T by TOPMETR:17;
reconsider E2a = E2a as continuous RealMap of T by TOPREAL6:74;
f1c - E2c is continuous RealMap of (T | A1) ;
then reconsider k = f1 - E2b as continuous Function of (T | A1),R^1 by TOPMETR:17, TOPREAL6:74;
reconsider f1c = f1c, E2c = E2c as continuous RealMap of (T | A1) ;
A16: ( dom f = the carrier of (T | A) & dom E2b = the carrier of (T | A) ) by FUNCT_2:def 1;
(2 / 3) |^ n > 0 by NEWTON:83;
then (2 / 3) * ((2 / 3) |^ n) > (2 / 3) * 0 by XREAL_1:68;
then (2 / 3) * ((2 / 3) |^ n) > 0 ;
then consider g being continuous Function of T,R^1 such that
A18: g, dom g is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n)) / 3 and
A19: k - g,A is_absolutely_bounded_by (2 * ((2 / 3) * ((2 / 3) |^ n))) / 3 by A1, A15, Th19;
reconsider ga = g as RealMap of T by TOPMETR:17;
reconsider ga = ga as continuous RealMap of T by TOPREAL6:74;
set y = E2a + ga;
reconsider y1 = E2a + ga as continuous Function of T,R^1 by TOPMETR:17, TOPREAL6:74;
( y1 in Funcs ( the carrier of T, the carrier of R^1) & y1 is continuous Function of T,R^1 ) by FUNCT_2:8;
then E2a + ga in D ;
then reconsider y = E2a + ga as Element of D ;
take y ; :: thesis:
take E2 ; :: thesis:
thus E2 = x by A11; :: thesis:
assume f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; :: thesis:
take g ; :: thesis:
thus y = E2 + g ; :: thesis:
A20: (2 / 3) * ((2 / 3) |^ n) = (2 / 3) |^ (n + 1) by NEWTON:6;
hence g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) by A18, FUNCT_2:def 1; :: thesis:
A21: dom g = the carrier of T by FUNCT_2:def 1;
A22: ((f - E2b) - g) | A = ((f - E2b) | A) - g by RFUNCT_1:47
.= (f - (E2b | A)) - g by RFUNCT_1:47
.= (f - (E2 | A)) - g by RELAT_1:72
.= ((f - E2) | A) - g by RFUNCT_1:47
.= ((f - E2) - g) | A by RFUNCT_1:47 ;
dom ((f - E2b) - g) = (dom (f - E2b)) /\ (dom g) by VALUED_1:12
.= ((dom f) /\ (dom E2b)) /\ (dom g) by VALUED_1:12
.= A by A3, A16, A21, XBOOLE_1:28 ;
hence (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) by A19, A20, A22, Th18; :: thesis:

end;

consider F being Function of NAT,D such that
A23: F . 0 = g0d and
A24: for n being Element of NAT holds S₁[n,F . n,F . (n + 1)] from RECDEF_1:sch 2(A10);

A25: now

let n be Element of NAT ; :: thesis:
S₁[n,F . n,F . (n + 1)] by A24;
hence F . n is PartFunc of the carrier of T,REAL by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6; :: thesis:

end;

dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Functional_Sequence of the carrier of T,REAL by A25, SEQFUNC:1;
consider E2 being continuous Function of T,R^1 such that
A26: E2 = F . 0 and
A27: ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ 0) implies ex g being continuous Function of T,R^1 st
( F . (0 + 1) = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (0 + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (0 + 1)) ) ) by A24;
(2 / 3) |^ 0 = 1 by NEWTON:4;
then consider g1 being continuous Function of T,R^1 such that
A28: F . (0 + 1) = E2 + g1 and
A29: g1, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (0 + 1)) and
(f - E2) - g1,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (0 + 1)) by A9, A23, A26, A27;
A30: dom g1 = the carrier of T by FUNCT_2:def 1
.= dom E2 by FUNCT_2:def 1 ;
defpred S₂[ Nat] means ( F . $1 is continuous Function of T,R^1 & (F . $1) - (F . ($1 + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power $1) & (F . $1) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power $1) );

A31: now

let n be Element of NAT ; :: thesis:
A32: dom f = [#] (T | A1) by FUNCT_2:def 1
.= A by PRE_TOPC:def 5 ;
consider E2 being continuous Function of T,R^1 such that
A33: ( E2 = F . n & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st
( F . (n + 1) = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) ) by A24;
assume S₂[n] ; :: thesis:
then (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) by POWER:41;
then consider g being continuous Function of T,R^1 such that
A34: F . (n + 1) = E2 + g and
g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) and
A35: (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) by A33, Th24;
A36: dom ((f - E2) - g) = (dom (f - E2)) /\ (dom g) by VALUED_1:12
.= ((dom f) /\ (dom E2)) /\ (dom g) by VALUED_1:12
.= ((dom f) /\ the carrier of T) /\ (dom g) by FUNCT_2:def 1
.= (dom f) /\ (dom g) by A32, XBOOLE_1:28
.= (dom f) /\ the carrier of T by FUNCT_2:def 1
.= A by A32, XBOOLE_1:28 ;
reconsider g9 = g as continuous RealMap of T by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6, TOPREAL6:74;
consider E3 being continuous Function of T,R^1 such that
A37: E3 = F . (n + 1) and
A38: ( f - E3,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) implies ex g being continuous Function of T,R^1 st
( F . ((n + 1) + 1) = E3 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) & (f - E3) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ((n + 1) + 1)) ) ) by A24;
A39: dom (f - (E2 + g)) = (dom f) /\ (dom (E2 + g)) by VALUED_1:12
.= A /\ ((dom E2) /\ (dom g)) by A32, VALUED_1:def 1
.= A /\ ((dom E2) /\ the carrier of T) by FUNCT_2:def 1
.= A /\ ( the carrier of T /\ the carrier of T) by FUNCT_2:def 1
.= A by XBOOLE_1:28 ;
A40: dom (f - E2) = A /\ (dom E2) by A32, VALUED_1:12
.= A /\ the carrier of T by FUNCT_2:def 1
.= A by XBOOLE_1:28 ;

A41: now

let a be set ; :: thesis:
assume A42: a in A ; :: thesis:
hence ((f - E2) - g) . a = ((f - E2) . a) - (g . a) by A36, VALUED_1:13
.= ((f . a) - (E2 . a)) - (g . a) by A40, A42, VALUED_1:13
.= (f . a) - ((E2 . a) + (g . a))
.= (f . a) - ((E2 + g) . a) by A42, VALUED_1:1
.= (f - (E2 + g)) . a by A39, A42, VALUED_1:13 ;
:: thesis:

end;

then consider gx being continuous Function of T,R^1 such that
A43: F . ((n + 1) + 1) = E3 + gx and
A44: gx, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) and
(f - E3) - gx,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ((n + 1) + 1)) by A34, A35, A37, A38, A36, A39, FUNCT_1:2;
A45: dom gx = the carrier of T by FUNCT_2:def 1
.= dom E3 by FUNCT_2:def 1 ;
reconsider E29 = E2 as continuous RealMap of T by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6, TOPREAL6:74;
A46: (2 / 9) * ((2 / 3) to_power (n + 1)) = ((1 / 3) * (2 / 3)) * ((2 / 3) |^ (n + 1)) by POWER:41
.= (1 / 3) * ((2 / 3) * ((2 / 3) |^ (n + 1)))
.= (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) by NEWTON:6 ;
A47: dom ((gx + E3) - E3) = (dom (gx + E3)) /\ (dom E3) by VALUED_1:12
.= ((dom gx) /\ (dom E3)) /\ (dom E3) by VALUED_1:def 1
.= dom gx by A45 ;

now

let a be set ; :: thesis:
assume A48: a in dom gx ; :: thesis:
hence ((gx + E3) - E3) . a = ((gx + E3) . a) - (E3 . a) by A47, VALUED_1:13
.= ((gx . a) + (E3 . a)) - (E3 . a) by A48, VALUED_1:1
.= gx . a ;
:: thesis:

end;

then A49: (F . ((n + 1) + 1)) - (F . (n + 1)) = gx by A37, A43, A47, FUNCT_1:2;
(f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) by A35, POWER:41;
then ( E29 + g9 is continuous RealMap of T & f - (F . (n + 1)),A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) ) by A34, A36, A39, A41, FUNCT_1:2;
hence S₂[n + 1] by A34, A44, A46, A49, Th24, METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6, TOPREAL6:74; :: thesis:

end;

A50: dom ((g1 + E2) - E2) = (dom (g1 + E2)) /\ (dom E2) by VALUED_1:12
.= ((dom g1) /\ (dom E2)) /\ (dom E2) by VALUED_1:def 1
.= dom g1 by A30 ;

now

let a be set ; :: thesis:
assume A51: a in dom g1 ; :: thesis:
hence ((g1 + E2) - E2) . a = ((g1 + E2) . a) - (E2 . a) by A50, VALUED_1:13
.= ((g1 . a) + (E2 . a)) - (E2 . a) by A51, VALUED_1:1
.= g1 . a ;
:: thesis:

end;

then A52: (F . (0 + 1)) - (F . 0) = g1 by A26, A28, A50, FUNCT_1:2;
( (2 / 3) to_power 0 = 1 & (1 / 3) * ((2 / 3) |^ 1) = (1 / 3) * (2 / 3) ) by NEWTON:5, POWER:24;
then A53: S₂[ 0 ] by A9, A23, A29, A52, Th24;
A54: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A53, A31);

A55: now

let n be natural number ; :: thesis:
n in NAT by ORDINAL1:def 12;
hence (F . n) - (F . (n + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n) by A54; :: thesis:

end;

( dom f = the carrier of (T | A1) & rng f c= REAL ) by FUNCT_2:def 1, VALUED_0:def 3;
then A56: f is Function of A1,REAL by A3, FUNCT_2:2;

now

let n be Element of NAT ; :: thesis:
S₁[n,F . n,F . (n + 1)] by A24;
hence the carrier of T c= dom (F . n) by FUNCT_2:def 1; :: thesis:

end;

then A57: the carrier of T common_on_dom F by SEQFUNC:def 9;
then A58: A1 common_on_dom F by SEQFUNC:23;

A59: now

let n be natural number ; :: thesis:
n in NAT by ORDINAL1:def 12;
hence (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n) by A54; :: thesis:

end;

A60: 2 / 9 > 0 ;
then F is_unif_conv_on the carrier of T by A57, A6, A55, Th11;
then reconsider h = lim (F, the carrier of T) as continuous Function of T,R^1 by A54, Th22;
F is_point_conv_on the carrier of T by A57, A60, A6, A55, Th11, SEQFUNC:22;
then A61: h | A1 = lim (F,A1) by SEQFUNC:24
.= f by A6, A59, A58, A56, Th13 ;
h, the carrier of T is_absolutely_bounded_by 1

proof

let x be set ; :: according to TIETZE:def 1 :: thesis:
assume x in the carrier of T /\ (dom h) ; :: thesis:
then reconsider z = x as Element of T ;
A62: dom (F . 0) = the carrier of T by A23, FUNCT_2:def 1;
then z in the carrier of T /\ (dom (F . 0)) ;
then A63: |.((F . 0) . z).| <= 1 / 3 by A8, A23, A62, Def1;
then (F . 0) . z >= - (1 / 3) by ABSVALUE:5;
then A64: ((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) >= (- (1 / 3)) - ((2 / 9) / (1 - (2 / 3))) by XREAL_1:9;
(F . 0) . z <= 1 / 3 by A63, ABSVALUE:5;
then A65: ((F . 0) . z) + ((2 / 9) / (1 - (2 / 3))) <= (1 / 3) + ((2 / 9) / (1 - (2 / 3))) by XREAL_1:7;
h . z <= ((F . 0) . z) + ((2 / 9) / (1 - (2 / 3))) by A57, A60, A6, A55, Th12;
then A66: h . z <= 1 by A65, XXREAL_0:2;
h . z >= ((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) by A57, A60, A6, A55, Th12;
then h . z >= - 1 by A64, XXREAL_0:2;
hence abs (h . x) <= 1 by A66, ABSVALUE:5; :: thesis:

end;

then reconsider h = h as Function of T,(Closed-Interval-TSpace ((- 1),1)) by Th23;
R^1 [.(- 1),1.] = [#] (Closed-Interval-TSpace ((- 1),1)) by A4, TOPREALB:def 3;
then Closed-Interval-TSpace ((- 1),1) = R^1 | (R^1 [.(- 1),1.]) by PRE_TOPC:def 5;
then h is continuous by TOPMETR:6;
hence ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f by A61; :: thesis:

end;