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 (Closed-Interval-TSpace (- 1),1) = [.(- 1),1.] by TOPMETR:25;
A4: the carrier of (T | A) = A by PRE_TOPC:29;

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 A6: rng (T --> (R^1 0 )) = {0 } by FUNCOP_1:14;
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 A6, TARSKI:def 1;
hence y in the carrier of (Closed-Interval-TSpace (- 1),1) by A3, XXREAL_1:1; :: thesis:

end;

then reconsider g = T --> (R^1 0 ) as Function of T,(Closed-Interval-TSpace (- 1),1) by FUNCT_2:8;
reconsider g = g as continuous Function of T,(Closed-Interval-TSpace (- 1),1) by PRE_TOPC:57;
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 } ;
T --> (R^1 0 ) is Element of Funcs the carrier of T,the carrier of R^1 by FUNCT_2:11;
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 ;
reconsider f1 = f as Function of (T | A1),R^1 by TOPREALA:28;
f1 is continuous by A2, PRE_TOPC:56;
then reconsider f1 = f as continuous Function of (T | A1),R^1 ;
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 5;
rng f1 c= the carrier of (Closed-Interval-TSpace (- 1),1) by RELAT_1:def 19;
then ( - 1 <= f1 . x & f1 . x <= 1 ) by A3, A7, XXREAL_1:1;
hence abs (f1 . x) <= 1 by ABSVALUE:12; :: 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:11;
then g0 in D ;
then reconsider g0d = g0 as Element of D ;
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)) ) ) );
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 & E2 is continuous Function of T,R^1 ) ;
reconsider E2 = E2 as continuous Function of T,R^1 by A11;

per cases ;

suppose A12: 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, A12; :: thesis:

end;

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

reconsider E2a = E2 as RealMap of T by TOPMETR:24;
reconsider E2a = E2a as continuous RealMap of T by TOPREAL6:83;
reconsider E2b = E2 | A as Function of (T | A1),R^1 by PRE_TOPC:30;
reconsider E2b = E2b as continuous Function of (T | A1),R^1 by TOPMETR:10;
E2b c= E2 by RELAT_1:88;
then A14: f - E2b,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) by A13, Th4, Th17;
set k = f1 - E2b;
reconsider k = f1 - E2b as Function of (T | A1),R^1 by TOPMETR:24;
reconsider f1c = f1, E2c = E2b as RealMap of (T | A1) by TOPMETR:24;
reconsider f1c = f1c, E2c = E2c as continuous RealMap of (T | A1) by TOPREAL6:83;
f1c - E2c is continuous ;
then A15: k is continuous by TOPREAL6:83;
set r = (2 / 3) * ((2 / 3) |^ n);
(2 / 3) |^ n > 0 by NEWTON:102;
then (2 / 3) * ((2 / 3) |^ n) > 0 by XREAL_1:131;
then consider g being continuous Function of T,R^1 such that
A16: g, dom g is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n)) / 3 and
A17: k - g,A is_absolutely_bounded_by (2 * ((2 / 3) * ((2 / 3) |^ n))) / 3 by A1, A14, A15, Th19;
reconsider ga = g as RealMap of T by TOPMETR:24;
reconsider ga = ga as continuous RealMap of T by TOPREAL6:83;
set y = E2a + ga;
reconsider y1 = E2a + ga as Function of T,R^1 by TOPMETR:24;
A18: y1 in Funcs the carrier of T,the carrier of R^1 by FUNCT_2:11;
y1 is continuous Function of T,R^1 by TOPREAL6:83;
then E2a + ga in D by A18;
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:
A19: (2 / 3) * ((2 / 3) |^ n) = (2 / 3) |^ (n + 1) by NEWTON:11;
hence g,the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) by A16, FUNCT_2:def 1; :: thesis:
A20: dom f = the carrier of (T | A) by FUNCT_2:def 1;
A21: dom E2b = the carrier of (T | A) by FUNCT_2:def 1;
A22: dom g = the carrier of T by FUNCT_2:def 1;
A23: 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 A4, A20, A21, A22, XBOOLE_1:28 ;
((f - E2b) - g) | A = ((f - E2b) | A) - g by RFUNCT_1:63
.= (f - (E2b | A)) - g by RFUNCT_1:63
.= (f - (E2 | A)) - g by RELAT_1:101
.= ((f - E2) | A) - g by RFUNCT_1:63
.= ((f - E2) - g) | A by RFUNCT_1:63 ;
hence (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) by A17, A19, A23, Th18; :: thesis:

end;

consider F being Function of NAT ,D such that
A24: F . 0 = g0d and
A25: for n being Element of NAT holds S₁[n,F . n,F . (n + 1)] from RECDEF_1:sch 2(A10);
A26: dom F = NAT by FUNCT_2:def 1;
A27: ( the carrier of RealSpace = REAL & the carrier of R^1 = REAL ) by METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7;

now

let n be Element of NAT ; :: thesis:
S₁[n,F . n,F . (n + 1)] by A25;
hence F . n is PartFunc of the carrier of T,REAL by METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7; :: thesis:

end;

then reconsider F = F as Functional_Sequence of the carrier of T,REAL by A26, SEQFUNC:1;

now

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

end;

then A28: the carrier of T common_on_dom F by SEQFUNC:def 10;
A29: ( 2 / 9 > 0 & 2 / 3 > 0 ) ;
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) );
consider E2 being continuous Function of T,R^1 such that
A30: ( E2 = F . 0 & ( 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 A25;
A31: ( (2 * 1) / 3 = (2 / 3) * 1 & (2 / 3) to_power 0 = 1 & (2 / 3) |^ 0 = 1 ) by NEWTON:9, POWER:29;
then consider g1 being continuous Function of T,R^1 such that
A32: ( F . (0 + 1) = E2 + g1 & g1,the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (0 + 1)) & (f - E2) - g1,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (0 + 1)) ) by A9, A24, A30;
A33: (1 / 3) * ((2 / 3) |^ 1) = (1 / 3) * (2 / 3) by NEWTON:10;
A34: dom g1 = the carrier of T by FUNCT_2:def 1
.= dom E2 by FUNCT_2:def 1 ;
A35: 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 A34 ;

now

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

end;

then ( (1 / 3) * ((2 / 3) |^ (0 + 1)) = (2 / 9) * 1 & (F . (0 + 1)) - (F . 0 ) = g1 ) by A30, A32, A33, A35, FUNCT_1:9;
then A37: S₂[ 0 ] by A9, A24, A31, A32, Th24;

A38: now

let n be Element of NAT ; :: thesis:
consider E2 being continuous Function of T,R^1 such that
A39: ( 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 A25;
assume S₂[n] ; :: thesis:
then (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) by POWER:46;
then consider g being continuous Function of T,R^1 such that
A40: ( 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 A39, Th24;
reconsider E2' = E2 as continuous RealMap of T by A27, TOPREAL6:83;
reconsider g' = g as continuous RealMap of T by A27, TOPREAL6:83;
A41: E2' + g' is continuous RealMap of T ;
consider E3 being continuous Function of T,R^1 such that
A42: ( E3 = F . (n + 1) & ( 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 A25;
A43: (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) by A40, POWER:46;
A44: dom f = [#] (T | A1) by FUNCT_2:def 1
.= A by PRE_TOPC:def 10 ;
A45: 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 A44, XBOOLE_1:28
.= (dom f) /\ the carrier of T by FUNCT_2:def 1
.= A by A44, XBOOLE_1:28 ;
A46: dom (f - (E2 + g)) = (dom f) /\ (dom (E2 + g)) by VALUED_1:12
.= A /\ ((dom E2) /\ (dom g)) by A44, 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 ;
A47: dom (f - E2) = A /\ (dom E2) by A44, VALUED_1:12
.= A /\ the carrier of T by FUNCT_2:def 1
.= A by XBOOLE_1:28 ;

A48: now

let a be set ; :: thesis:
assume A49: a in A ; :: thesis:
hence ((f - E2) - g) . a = ((f - E2) . a) - (g . a) by A45, VALUED_1:13
.= ((f . a) - (E2 . a)) - (g . a) by A47, A49, VALUED_1:13
.= (f . a) - ((E2 . a) + (g . a))
.= (f . a) - ((E2 + g) . a) by A49, VALUED_1:1
.= (f - (E2 + g)) . a by A46, A49, VALUED_1:13 ;
:: thesis:

end;

then A50: f - (F . (n + 1)),A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) by A40, A43, A45, A46, FUNCT_1:9;
consider gx being continuous Function of T,R^1 such that
A51: ( F . ((n + 1) + 1) = E3 + gx & gx,the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) & (f - E3) - gx,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ((n + 1) + 1)) ) by A40, A42, A45, A46, A48, FUNCT_1:9;
A52: (2 / 9) * ((2 / 3) to_power (n + 1)) = ((1 / 3) * (2 / 3)) * ((2 / 3) |^ (n + 1)) by POWER:46
.= (1 / 3) * ((2 / 3) * ((2 / 3) |^ (n + 1)))
.= (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) by NEWTON:11 ;
A53: dom gx = the carrier of T by FUNCT_2:def 1
.= dom E3 by FUNCT_2:def 1 ;
A54: 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 A53 ;

now

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

end;

then (F . ((n + 1) + 1)) - (F . (n + 1)) = gx by A42, A51, A54, FUNCT_1:9;
hence S₂[n + 1] by A27, A40, A41, A50, A51, A52, Th24, TOPREAL6:83; :: thesis:

end;

A56: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A37, A38);

A57: now

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

end;

then A58: F is_unif_conv_on the carrier of T by A28, A29, Th11;
then reconsider h = lim F,the carrier of T as continuous Function of T,R^1 by A56, Th22;

A59: now

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

end;

A60: A1 common_on_dom F by A28, SEQFUNC:24;
( dom f = the carrier of (T | A1) & rng f c= REAL ) by FUNCT_2:def 1, VALUED_0:def 3;
then A61: f is Function of A1,REAL by A4, FUNCT_2:4;
F is_point_conv_on the carrier of T by A58, SEQFUNC:23;
then A62: h | A1 = lim F,A1 by SEQFUNC:25
.= f by A29, A59, A60, A61, 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 ;
dom (F . 0 ) = the carrier of T by A24, FUNCT_2:def 1;
then ( z in the carrier of T /\ (dom (F . 0 )) & F . 0 ,the carrier of T is_absolutely_bounded_by 1 / 3 ) by A8, A24;
then |.((F . 0 ) . z).| <= 1 / 3 by Def1;
then ( (F . 0 ) . z >= - (1 / 3) & (F . 0 ) . z <= 1 / 3 ) by ABSVALUE:12;
then ( ((F . 0 ) . z) - ((2 / 9) / (1 - (2 / 3))) >= (- (1 / 3)) - ((2 / 9) / (1 - (2 / 3))) & ((F . 0 ) . z) + ((2 / 9) / (1 - (2 / 3))) <= (1 / 3) + ((2 / 9) / (1 - (2 / 3))) & h . z >= ((F . 0 ) . z) - ((2 / 9) / (1 - (2 / 3))) & h . z <= ((F . 0 ) . z) + ((2 / 9) / (1 - (2 / 3))) ) by A28, A29, A57, Th12, XREAL_1:9, XREAL_1:11;
then ( h . z >= - 1 & h . z <= 1 ) by XXREAL_0:2;
hence abs (h . x) <= 1 by ABSVALUE:12; :: 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 A3, TOPREALB:def 3;
then Closed-Interval-TSpace (- 1),1 = R^1 | (R^1 [.(- 1),1.]) by PRE_TOPC:def 10;
then h is continuous by TOPMETR:9;
hence ex g being continuous Function of T,(Closed-Interval-TSpace (- 1),1) st g | A = f by A62; :: thesis:

end;