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:8;
A4: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18;
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:8;
rng (T --> (R^1 0)) c= the carrier of (Closed-Interval-TSpace ((- 1),1))
proof
let y be object ; :: 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:6;
reconsider g = g as continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) by PRE_TOPC:27;
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:7;
defpred S1[ 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: ( x in A /\ (dom f1) implies |.(f1 . x).| <= 1 )
assume x in A /\ (dom f1) ; :: thesis: |.(f1 . x).| <= 1
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 |.(f1 . x).| <= 1 by ABSVALUE:5; :: 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, Th17;
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 Nat
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be 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: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, Th2, Th15;
set r = (2 / 3) * ((2 / 3) |^ n);
reconsider f1c = f1, E2c = E2b as continuous RealMap of (T | A1) by JORDAN5A:27, TOPMETR:17;
set k = f1 - E2b;
reconsider E2a = E2 as RealMap of T by TOPMETR:17;
reconsider E2a = E2a as continuous RealMap of T by JORDAN5A:27;
f1c - E2c is continuous RealMap of (T | A1) ;
then reconsider k = f1 - E2b as continuous Function of (T | A1),R^1 by JORDAN5A:27, TOPMETR:17;
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
A17: g, dom g is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n)) / 3 and
A18: k - g,A is_absolutely_bounded_by (2 * ((2 / 3) * ((2 / 3) |^ n))) / 3 by A1, A15, Th17;
reconsider ga = g as RealMap of T by TOPMETR:17;
reconsider ga = ga as continuous RealMap of T by JORDAN5A:27;
set y = E2a + ga;
reconsider y1 = E2a + ga as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
( 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: 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)) )
A19: (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 A17, FUNCT_2:def 1; :: thesis: (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1))
A20: dom g = the carrier of T by FUNCT_2:def 1;
A21: ((f - E2b) - g) | A = ((f - E2b) | A) - g by RFUNCT_1:47
.= (f - (E2b | A)) - g
.= (f - (E2 | A)) - g
.= ((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, A20, XBOOLE_1:28 ;
hence (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) by A18, A19, A21, Th16; :: thesis: verum
end;
end;
end;
consider F being sequence of D such that
A22: F . 0 = g0d and
A23: for n being Nat holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch 2(A10);
A24: now :: thesis: for n being Nat holds F . n is PartFunc of the carrier of T,REAL
let n be Nat; :: thesis: F . n is PartFunc of the carrier of T,REAL
S1[n,F . n,F . (n + 1)] by A23;
hence F . n is PartFunc of the carrier of T,REAL by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6; :: 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 A24, SEQFUNC:1;
consider E2 being continuous Function of T,R^1 such that
A25: E2 = F . 0 and
A26: ( 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 A23;
(2 / 3) |^ 0 = 1 by NEWTON:4;
then consider g1 being continuous Function of T,R^1 such that
A27: F . (0 + 1) = E2 + g1 and
A28: 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, A22, A25, A26;
A29: 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) );
A30: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
A31: 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
A32: ( 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 A23;
assume S2[n] ; :: thesis: S2[n + 1]
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
A33: F . (n + 1) = E2 + g and
g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) and
A34: (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) by A32, Th22;
A35: 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 A31, XBOOLE_1:28
.= (dom f) /\ the carrier of T by FUNCT_2:def 1
.= A by A31, XBOOLE_1:28 ;
reconsider g9 = g as continuous RealMap of T by JORDAN5A:27, METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;
consider E3 being continuous Function of T,R^1 such that
A36: E3 = F . (n + 1) and
A37: ( 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 A23;
A38: dom (f - (E2 + g)) = (dom f) /\ (dom (E2 + g)) by VALUED_1:12
.= A /\ ((dom E2) /\ (dom g)) by A31, 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 ;
A39: dom (f - E2) = A /\ (dom E2) by A31, VALUED_1:12
.= A /\ the carrier of T by FUNCT_2:def 1
.= A by XBOOLE_1:28 ;
A40: now :: thesis: for a being object st a in A holds
((f - E2) - g) . a = (f - (E2 + g)) . a
let a be object ; :: thesis: ( a in A implies ((f - E2) - g) . a = (f - (E2 + g)) . a )
assume A41: a in A ; :: thesis: ((f - E2) - g) . a = (f - (E2 + g)) . a
hence ((f - E2) - g) . a = ((f - E2) . a) - (g . a) by A35, VALUED_1:13
.= ((f . a) - (E2 . a)) - (g . a) by A39, A41, VALUED_1:13
.= (f . a) - ((E2 . a) + (g . a))
.= (f . a) - ((E2 + g) . a) by A41, VALUED_1:1
.= (f - (E2 + g)) . a by A38, A41, VALUED_1:13 ;
:: thesis: verum
end;
then consider gx being continuous Function of T,R^1 such that
A42: F . ((n + 1) + 1) = E3 + gx and
A43: 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 A33, A34, A36, A37, A35, A38, FUNCT_1:2;
A44: 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 JORDAN5A:27, METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;
A45: (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 ;
A46: 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 A44 ;
now :: thesis: for a being object st a in dom gx holds
((gx + E3) - E3) . a = gx . a
let a be object ; :: thesis: ( a in dom gx implies ((gx + E3) - E3) . a = gx . a )
assume A47: a in dom gx ; :: thesis: ((gx + E3) - E3) . a = gx . a
hence ((gx + E3) - E3) . a = ((gx + E3) . a) - (E3 . a) by A46, VALUED_1:13
.= ((gx . a) + (E3 . a)) - (E3 . a) by A47, VALUED_1:1
.= gx . a ;
:: thesis: verum
end;
then A48: (F . ((n + 1) + 1)) - (F . (n + 1)) = gx by A36, A42, A46, FUNCT_1:2;
(f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) by A34, 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 A33, A35, A38, A40, FUNCT_1:2;
hence S2[n + 1] by A33, A43, A45, A48, Th22, JORDAN5A:27, METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6; :: thesis: verum
end;
A49: 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 A29 ;
now :: thesis: for a being object st a in dom g1 holds
((g1 + E2) - E2) . a = g1 . a
let a be object ; :: thesis: ( a in dom g1 implies ((g1 + E2) - E2) . a = g1 . a )
assume A50: a in dom g1 ; :: thesis: ((g1 + E2) - E2) . a = g1 . a
hence ((g1 + E2) - E2) . a = ((g1 + E2) . a) - (E2 . a) by A49, VALUED_1:13
.= ((g1 . a) + (E2 . a)) - (E2 . a) by A50, VALUED_1:1
.= g1 . a ;
:: thesis: verum
end;
then A51: (F . (0 + 1)) - (F . 0) = g1 by A25, A27, A49, FUNCT_1:2;
( (2 / 3) to_power 0 = 1 & (1 / 3) * ((2 / 3) |^ 1) = (1 / 3) * (2 / 3) ) by POWER:24;
then A52: S2[ 0 ] by A9, A22, A28, A51, Th22;
A53: for n being Nat holds S2[n] from NAT_1:sch 2(A52, A30);
A54: for n being Nat holds (F . n) - (F . (n + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n) by A53;
( dom f = the carrier of (T | A1) & rng f c= REAL ) by FUNCT_2:def 1, VALUED_0:def 3;
then A55: f is Function of A1,REAL by A3, FUNCT_2:2;
now :: thesis: for n being Nat holds the carrier of T c= dom (F . n)
let n be Nat; :: thesis: the carrier of T c= dom (F . n)
S1[n,F . n,F . (n + 1)] by A23;
hence the carrier of T c= dom (F . n) by FUNCT_2:def 1; :: thesis: verum
end;
then A56: the carrier of T common_on_dom F ;
then A57: A1 common_on_dom F by SEQFUNC:23;
A58: for n being Nat holds (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n) by A53;
A59: 2 / 9 > 0 ;
then F is_unif_conv_on the carrier of T by A56, A6, A54, Th9;
then reconsider h = lim (F, the carrier of T) as continuous Function of T,R^1 by A53, Th20;
F is_point_conv_on the carrier of T by A56, A59, A6, A54, Th9, SEQFUNC:22;
then A60: h | A1 = lim (F,A1) by SEQFUNC:24
.= f by A6, A58, A57, A55, Th11 ;
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 |.(h . x).| <= 1 )
assume x in the carrier of T /\ (dom h) ; :: thesis: |.(h . x).| <= 1
then reconsider z = x as Element of T ;
A61: dom (F . 0) = the carrier of T by A22, FUNCT_2:def 1;
A62: |.((F . 0) . z).| <= 1 / 3 by A8, A22, A61;
then (F . 0) . z >= - (1 / 3) by ABSVALUE:5;
then A63: ((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 A62, ABSVALUE:5;
then A64: ((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 A56, A59, A6, A54, Th10;
then A65: h . z <= 1 by A64, XXREAL_0:2;
h . z >= ((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) by A56, A59, A6, A54, Th10;
then h . z >= - 1 by A63, XXREAL_0:2;
hence |.(h . x).| <= 1 by A65, ABSVALUE:5; :: thesis: verum
end;
then reconsider h = h as Function of T,(Closed-Interval-TSpace ((- 1),1)) by Th21;
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 A60; :: thesis: verum
end;
end;