let T be non empty TopSpace; :: thesis: ( T is normal implies for A being closed Subset of T
for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds
ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f )
assume A1: T is normal ; :: thesis: for A being closed Subset of T
for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds
ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
let A be closed Subset of T; :: thesis: for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds
ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
let f be Function of (T | A),(Closed-Interval-TSpace ((- 1),1)); :: thesis: ( f is continuous implies ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f )
assume A2: f is continuous ; :: thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
A3: the carrier of (T | A) = A by PRE_TOPC:29;
A4: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:25;
per cases ( A is empty or not A is empty ) ;
suppose A is empty ; :: thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
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: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: ( not y in rng (T --> (R^1 0)) or y in the carrier of (Closed-Interval-TSpace ((- 1),1)) )
assume y in rng (T --> (R^1 0)) ; :: thesis: y in the carrier of (Closed-Interval-TSpace ((- 1),1))
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: verum
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 | A = f
g | A1 is empty ;
hence g | A = f ; :: thesis: verum
end;
suppose not A is empty ; :: thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f
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:28;
defpred S1[ 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:56;
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: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 ;
f1,A is_absolutely_bounded_by 1
proof
let x be set ; :: according to TIETZE:def 1 :: thesis: ( x in A /\ (dom f1) implies abs (f1 . x) <= 1 )
assume x in A /\ (dom f1) ; :: thesis: abs (f1 . x) <= 1
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 A4, A7, XXREAL_1:1;
hence abs (f1 . x) <= 1 by ABSVALUE:12; :: thesis: verum
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 ;
A10: for n being Element of NAT
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be Element of NAT ; :: thesis: for x being Element of D ex y being Element of D st S1[n,x,y]
let x be Element of D; :: thesis: ex y being Element of D st S1[n,x,y]
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 ( not f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) or f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ) ;
suppose A13: not f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; :: thesis: ex y being Element of D st S1[n,x,y]
take x ; :: thesis: S1[n,x,x]
take E2 ; :: thesis: ( 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)) ) ) )
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: verum
end;
suppose A14: f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; :: thesis: ex y being Element of D st S1[n,x,y]
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 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 RealMap of (T | A1) by TOPMETR:24;
set k = f1 - E2b;
reconsider E2a = E2 as RealMap of T by TOPMETR:24;
reconsider E2a = E2a as continuous RealMap of T by TOPREAL6:83;
reconsider k = f1 - E2b as Function of (T | A1),R^1 by TOPMETR:24;
reconsider f1c = f1c, E2c = E2c as continuous RealMap of (T | A1) by TOPREAL6:83;
A16: ( dom f = the carrier of (T | A) & dom E2b = the carrier of (T | A) ) by FUNCT_2:def 1;
f1c - E2c is continuous ;
then A17: k is continuous by TOPREAL6:83;
(2 / 3) |^ n > 0 by NEWTON:102;
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, A17, Th19, XREAL_1:131;
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;
( y1 in Funcs ( the carrier of T, the carrier of R^1) & y1 is continuous Function of T,R^1 ) by FUNCT_2:11, TOPREAL6:83;
then E2a + ga in D ;
then reconsider y = E2a + ga as Element of D ;
take y ; :: thesis: S1[n,x,y]
take E2 ; :: thesis: ( 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
( y = 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)) ) ) )
thus E2 = x by A11; :: thesis: ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st
( y = 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)) ) )
assume f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; :: thesis: ex g being continuous Function of T,R^1 st
( y = 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)) )
take g ; :: thesis: ( y = 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)) )
thus y = E2 + g ; :: thesis: ( 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)) )
A20: (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 A18, FUNCT_2:def 1; :: thesis: (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1))
A21: dom g = the carrier of T by FUNCT_2:def 1;
A22: ((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 ;
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: verum
end;
end;
end;
consider F being Function of NAT,D such that
A23: F . 0 = g0d and
A24: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch 2(A10);
A25: now
let n be Element of NAT ; :: thesis: F . n is PartFunc of the carrier of T,REAL
S1[n,F . n,F . (n + 1)] by A24;
hence F . n is PartFunc of the carrier of T,REAL by METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7; :: thesis: verum
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:9;
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 S2[ 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: ( S2[n] implies S2[n + 1] )
A32: dom f = [#] (T | A1) by FUNCT_2:def 1
.= A by PRE_TOPC:def 10 ;
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 S2[n] ; :: thesis: S2[n + 1]
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
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 14, TOPMETR:16, TOPMETR:def 7, TOPREAL6:83;
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: ( a in A implies ((f - E2) - g) . a = (f - (E2 + g)) . a )
assume A42: a in A ; :: thesis: ((f - E2) - g) . a = (f - (E2 + g)) . a
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: verum
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:9;
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 14, TOPMETR:16, TOPMETR:def 7, TOPREAL6:83;
A46: (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 ;
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: ( a in dom gx implies ((gx + E3) - E3) . a = gx . a )
assume A48: a in dom gx ; :: thesis: ((gx + E3) - E3) . a = gx . a
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: verum
end;
then A49: (F . ((n + 1) + 1)) - (F . (n + 1)) = gx by A37, A43, A47, FUNCT_1:9;
(f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) by A35, POWER:46;
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:9;
hence S2[n + 1] by A34, A44, A46, A49, Th24, METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7, TOPREAL6:83; :: thesis: verum
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: ( a in dom g1 implies ((g1 + E2) - E2) . a = g1 . a )
assume A51: a in dom g1 ; :: thesis: ((g1 + E2) - E2) . a = g1 . a
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: verum
end;
then A52: (F . (0 + 1)) - (F . 0) = g1 by A26, A28, A50, FUNCT_1:9;
( (2 / 3) to_power 0 = 1 & (1 / 3) * ((2 / 3) |^ 1) = (1 / 3) * (2 / 3) ) by NEWTON:10, POWER:29;
then A53: S2[ 0 ] by A9, A23, A29, A52, Th24;
A54: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A53, A31);
A55: now
let n be natural number ; :: thesis: (F . n) - (F . (n + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n)
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 A54; :: thesis: verum
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:4;
now
let n be Element of NAT ; :: thesis: the carrier of T c= dom (F . n)
S1[n,F . n,F . (n + 1)] by A24;
hence the carrier of T c= dom (F . n) by FUNCT_2:def 1; :: thesis: verum
end;
then A57: the carrier of T common_on_dom F by SEQFUNC:def 10;
then A58: A1 common_on_dom F by SEQFUNC:24;
A59: now
let n be natural number ; :: thesis: (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n)
n in NAT by ORDINAL1:def 13;
hence (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n) by A54; :: thesis: verum
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:23;
then A61: h | A1 = lim (F,A1) by SEQFUNC:25
.= 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: ( x in the carrier of T /\ (dom h) implies abs (h . x) <= 1 )
assume x in the carrier of T /\ (dom h) ; :: thesis: abs (h . x) <= 1
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:12;
then A64: ((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) >= (- (1 / 3)) - ((2 / 9) / (1 - (2 / 3))) by XREAL_1:11;
(F . 0) . z <= 1 / 3 by A63, ABSVALUE:12;
then A65: ((F . 0) . z) + ((2 / 9) / (1 - (2 / 3))) <= (1 / 3) + ((2 / 9) / (1 - (2 / 3))) by XREAL_1:9;
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:12; :: thesis: verum
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 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 A61; :: thesis: verum
end;
end;