let M be non empty MetrSpace; :: thesis: for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let T be NormedLinearTopSpace; :: thesis: ( S = TopSpaceMetr M & T is complete implies for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous ) )
assume A1: ( S = TopSpaceMetr M & T is complete ) ; :: thesis: for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); :: thesis: for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let H be non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))); :: thesis: ( G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded implies ( G is equibounded & G is equicontinuous ) )
assume A2: G = H ; :: thesis: ( not (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded or ( G is equibounded & G is equicontinuous ) )
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
set MZH = (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H;
A3: the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) = H by TOPMETR:def 2;
assume A4: (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ; :: thesis: ( G is equibounded & G is equicontinuous )
consider L being Subset-Family of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A5: ( L is finite & the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) = union L & ( for C being Subset of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st C in L holds
ex w being Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st C = Ball (w,1) ) ) by A4;
defpred S₁[ object , object ] means ex w being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( $2 = w & $1 = Ball (w,1) );
A6: for D being object st D in L holds
ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₁[D,w] )

proof

let D be object ; :: thesis: ( D in L implies ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₁[D,w] ) )
assume A7: D in L ; :: thesis: ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₁[D,w] )
then reconsider D0 = D as Subset of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
consider w being Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A8: D0 = Ball (w,1) by A5, A7;
take w ; :: thesis: ( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₁[D,w] )
thus ( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₁[D,w] ) by A8; :: thesis: verum

end;

consider U being Function of L, the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A9: for D being object st D in L holds
S₁[D,U . D] from FUNCT_2:sch 1(A6);
A10: for D being object st D in L holds
D = Ball ((U /. D),1)

proof

let D be object ; :: thesis: ( D in L implies D = Ball ((U /. D),1) )
assume A11: D in L ; :: thesis: D = Ball ((U /. D),1)
then A12: ex x0 being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( U . D = x0 & D = Ball (x0,1) ) by A9;
dom U = L by FUNCT_2:def 1;
hence D = Ball ((U /. D),1) by A12, A11, PARTFUN1:def 6; :: thesis: verum

end;

set NF = the normF of (R_NormSpace_of_ContinuousFunctions (S,T));
A13: dom U = L by FUNCT_2:def 1;
reconsider NFU = the normF of (R_NormSpace_of_ContinuousFunctions (S,T)) .: (rng U) as finite Subset of REAL by A5;
consider xx being object such that
A14: xx in L by XBOOLE_0:def 1, A5, ZFMISC_1:2;
rng U <> {} by A13, A14, FUNCT_1:3;
then consider xx being object such that
A15: xx in rng U by XBOOLE_0:def 1;
reconsider xx = xx as Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A15;
set d0 = upper_bound NFU;
A16: for r being Real st r in NFU holds
r <= upper_bound NFU by SEQ_4:def 1;
set K = (upper_bound NFU) + 1;
for f being Function of the carrier of M, the carrier of T st f in G holds
for x being Element of M holds ||.(f . x).|| <= (upper_bound NFU) + 1

proof

let f be Function of the carrier of M, the carrier of T; :: thesis: ( f in G implies for x being Element of M holds ||.(f . x).|| <= (upper_bound NFU) + 1 )
assume f in G ; :: thesis: for x being Element of M holds ||.(f . x).|| <= (upper_bound NFU) + 1
then consider C being set such that
A17: ( f in C & C in L ) by A5, TARSKI:def 4, A3, A2;
reconsider C = C as Subset of the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A17;
reconsider pf = f as Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A17;
A18: pf in H by A3;
set pg = U /. C;
reconsider pg = U /. C as Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
A19: C = Ball (pg,1) by A10, A17;
A20: pg in H by A3;
then pg in R_NormSpace_of_ContinuousFunctions (S,T) ;
then ex f being Function of the carrier of S, the carrier of T st
( pg = f & f is continuous ) ;
then reconsider g = pg as Function of S,T ;
pf in { y where y is Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) : dist (pg,y) < 1 } by METRIC_1:def 14, A17, A19;
then A21: ex y being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( pf = y & dist (pg,y) < 1 ) ;
reconsider ppf = pf, ppg = pg as Element of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) by A18, A20;
A22: dist (ppg,ppf) < 1 by A21, TOPMETR:def 1;
reconsider pppf = ppf, pppg = ppg as Point of (R_NormSpace_of_ContinuousFunctions (S,T)) ;
A23: ||.(pppg - pppf).|| < 1 by A22, NORMSP_2:def 1;
pppf = (pppf - pppg) + pppg by RLVECT_4:1;
then ||.pppf.|| <= ||.(pppf - pppg).|| + ||.pppg.|| by NORMSP_1:def 1;
then A24: ||.pppf.|| <= ||.(pppg - pppf).|| + ||.pppg.|| by NORMSP_1:7;
A25: C in dom U by FUNCT_2:def 1, A17;
U . C in rng U by FUNCT_1:3, A13, A17;
then pg in rng U by A25, PARTFUN1:def 6;
then ||.pppg.|| <= upper_bound NFU by A16, FUNCT_2:35;
then ||.(pppg - pppf).|| + ||.pppg.|| <= 1 + (upper_bound NFU) by XREAL_1:8, A23;
then A26: ||.pppf.|| <= (upper_bound NFU) + 1 by A24, XXREAL_0:2;
let x be Element of M; :: thesis: ||.(f . x).|| <= (upper_bound NFU) + 1
reconsider x0 = x as Point of S by A1;
reconsider f0 = f as Function of the carrier of S, the carrier of T by A1;
||.(f0 . x0).|| <= ||.pppf.|| by C0SP3:37;
hence ||.(f . x).|| <= (upper_bound NFU) + 1 by A26, XXREAL_0:2; :: thesis: verum

end;

hence G is equibounded ; :: thesis: G is equicontinuous
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) ) )
assume A27: 0 < e ; :: thesis: ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) )
then consider L being Subset-Family of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A28: ( L is finite & the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) = union L & ( for C being Subset of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st C in L holds
ex w being Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st C = Ball (w,(e / 3)) ) ) by A4;
defpred S₂[ object , object ] means ex w being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( $2 = w & $1 = Ball (w,(e / 3)) );
A29: for D being object st D in L holds
ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₂[D,w] )

proof

let D be object ; :: thesis: ( D in L implies ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₂[D,w] ) )
assume A30: D in L ; :: thesis: ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₂[D,w] )
then reconsider D0 = D as Subset of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
consider w being Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A31: D0 = Ball (w,(e / 3)) by A28, A30;
take w ; :: thesis: ( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₂[D,w] )
thus ( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S₂[D,w] ) by A31; :: thesis: verum

end;

consider U being Function of L, the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A32: for D being object st D in L holds
S₂[D,U . D] from FUNCT_2:sch 1(A29);
A33: for D being object st D in L holds
D = Ball ((U /. D),(e / 3))

proof

let D be object ; :: thesis: ( D in L implies D = Ball ((U /. D),(e / 3)) )
assume A34: D in L ; :: thesis: D = Ball ((U /. D),(e / 3))
then A35: ex x0 being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( U . D = x0 & D = Ball (x0,(e / 3)) ) by A32;
dom U = L by FUNCT_2:def 1;
hence D = Ball ((U /. D),(e / 3)) by A35, A34, PARTFUN1:def 6; :: thesis: verum

end;

defpred S₃[ Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H), Real] means ex f being Function of the carrier of S, the carrier of T st
( $1 = f & 0 < $2 & ( for x1, x2 being Point of M st dist (x1,x2) < $2 holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) );
A36: for x0 being Element of the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ex d being Element of REAL st S₃[x0,d]

proof

let x0 be Element of the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H); :: thesis: ex d being Element of REAL st S₃[x0,d]
x0 in H by A3;
then x0 in R_NormSpace_of_ContinuousFunctions (S,T) ;
then A37: ex f being Function of the carrier of S, the carrier of T st
( x0 = f & f is continuous ) ;
then reconsider f = x0 as Function of the carrier of S, the carrier of T ;
consider d being Real such that
A38: ( 0 < d & ( for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) ) by A27, Th4, A1, A37;
reconsider d0 = d as Element of REAL by XREAL_0:def 1;
take d0 ; :: thesis: S₃[x0,d0]
thus S₃[x0,d0] by A38; :: thesis: verum

end;

consider NF being Function of the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H),REAL such that
A39: for f being Element of the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) holds S₃[f,NF . f] from FUNCT_2:sch 3(A36);
A40: dom U = L by FUNCT_2:def 1;
reconsider NFU = NF .: (rng U) as finite Subset of REAL by A28;
consider xx being object such that
A41: xx in L by XBOOLE_0:def 1, A28, ZFMISC_1:2;
rng U <> {} by A40, A41, FUNCT_1:3;
then consider xx being object such that
A42: xx in rng U by XBOOLE_0:def 1;
reconsider xx = xx as Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A42;
A43: ( NFU is bounded_below & lower_bound NFU in NFU ) by SEQ_4:133, A42;
set d = lower_bound NFU;
consider xx being object such that
A44: ( xx in dom NF & xx in rng U & lower_bound NFU = NF . xx ) by FUNCT_1:def 6, A43;
reconsider xx = xx as Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A44;
A45: ex f being Function of the carrier of S, the carrier of T st
( xx = f & 0 < NF . xx & ( for x1, x2 being Point of M st dist (x1,x2) < NF . xx holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) ) by A39;
take lower_bound NFU ; :: thesis: ( 0 < lower_bound NFU & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f . x1) - (f . x2)).|| < e ) )
thus 0 < lower_bound NFU by A45, A44; :: thesis: for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f . x1) - (f . x2)).|| < e
thus for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f . x1) - (f . x2)).|| < e :: thesis: verum

proof

let f0 be Function of the carrier of M, the carrier of T; :: thesis: ( f0 in G implies for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f0 . x1) - (f0 . x2)).|| < e )
assume f0 in G ; :: thesis: for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f0 . x1) - (f0 . x2)).|| < e
then consider C being set such that
A46: ( f0 in C & C in L ) by A28, TARSKI:def 4, A3, A2;
reconsider f = f0 as Function of the carrier of S, the carrier of T by A1;
reconsider C = C as Subset of the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A46;
reconsider pf = f0 as Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A46;
A47: pf in H by A3;
reconsider pg = U /. C as Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
A48: C = Ball (pg,(e / 3)) by A33, A46;
A49: pg in H by A3;
then pg in ContinuousFunctions (S,T) ;
then ex f being Function of the carrier of S, the carrier of T st
( pg = f & f is continuous ) ;
then reconsider g = pg as Function of S,T ;
pf in { y where y is Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) : dist (pg,y) < e / 3 } by METRIC_1:def 14, A46, A48;
then A50: ex y being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( pf = y & dist (pg,y) < e / 3 ) ;
reconsider ppf = pf, ppg = pg as Element of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) by A47, A49;
A51: dist (ppg,ppf) < e / 3 by A50, TOPMETR:def 1;
reconsider pppf = ppf, pppg = ppg as Point of (R_NormSpace_of_ContinuousFunctions (S,T)) ;
A52: ||.(pppg - pppf).|| < e / 3 by A51, NORMSP_2:def 1;
A53: C in dom U by FUNCT_2:def 1, A46;
U . C in rng U by FUNCT_1:3, A40, A46;
then pg in rng U by A53, PARTFUN1:def 6;
then A54: NF . pppg in NF .: (rng U) by FUNCT_2:35;
let x1, x2 be Element of M; :: thesis: ( dist (x1,x2) < lower_bound NFU implies ||.((f0 . x1) - (f0 . x2)).|| < e )
reconsider x10 = x1, x20 = x2 as Point of S by A1;
assume A55: dist (x1,x2) < lower_bound NFU ; :: thesis: ||.((f0 . x1) - (f0 . x2)).|| < e
lower_bound NFU <= NF . pg by A54, SEQ_4:def 2;
then A56: dist (x1,x2) < NF . pg by A55, XXREAL_0:2;
ex f being Function of the carrier of S, the carrier of T st
( pg = f & 0 < NF . pg & ( for x1, x2 being Point of M st dist (x1,x2) < NF . pg holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) ) by A39;
then A57: ||.((g /. x1) - (g /. x2)).|| < e / 3 by A56;
pppg - pppf in ContinuousFunctions (S,T) ;
then ex f being Function of the carrier of S, the carrier of T st
( pppg - pppf = f & f is continuous ) ;
then reconsider gf = pppg - pppf as Function of S,T ;
pppf - pppg in ContinuousFunctions (S,T) ;
then ex f being Function of the carrier of S, the carrier of T st
( pppf - pppg = f & f is continuous ) ;
then reconsider fg = pppf - pppg as Function of S,T ;
||.(gf . x20).|| <= ||.(pppg - pppf).|| by C0SP3:37;
then A59: ||.((g . x20) - (f . x20)).|| <= ||.(pppg - pppf).|| by C0SP3:48;
( f /. x20 = f . x20 & g /. x20 = g . x20 ) ;
then A60: ||.((g /. x2) - (f /. x2)).|| < e / 3 by A59, XXREAL_0:2, A52;
||.(fg . x10).|| <= ||.(pppf - pppg).|| by C0SP3:37;
then ||.((f . x10) - (g . x10)).|| <= ||.(pppf - pppg).|| by C0SP3:48;
then A62: ||.((f . x10) - (g . x10)).|| <= ||.(pppg - pppf).|| by NORMSP_1:7;
( f /. x10 = f . x10 & g /. x10 = g . x10 ) ;
then A63: ||.((f /. x1) - (g /. x1)).|| < e / 3 by A62, XXREAL_0:2, A52;
(f /. x1) - (f /. x2) = (((f /. x1) - (g /. x1)) + (g /. x1)) - (f /. x2) by RLVECT_4:1
.= ((f /. x1) - (g /. x1)) + ((g /. x1) - (f /. x2)) by RLVECT_1:28
.= ((f /. x1) - (g /. x1)) + ((((g /. x1) - (g /. x2)) + (g /. x2)) - (f /. x2)) by RLVECT_4:1
.= ((f /. x1) - (g /. x1)) + (((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))) by RLVECT_1:28 ;
then A64: ||.((f /. x1) - (f /. x2)).|| <= ||.((f /. x1) - (g /. x1)).|| + ||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).|| by NORMSP_1:def 1;
A65: ||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).|| <= ||.((g /. x1) - (g /. x2)).|| + ||.((g /. x2) - (f /. x2)).|| by NORMSP_1:def 1;
||.((g /. x1) - (g /. x2)).|| + ||.((g /. x2) - (f /. x2)).|| < (e / 3) + (e / 3) by A57, A60, XREAL_1:8;
then ||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).|| < (e / 3) + (e / 3) by XXREAL_0:2, A65;
then A66: ||.((f /. x1) - (g /. x1)).|| + ||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).|| < (e / 3) + ((e / 3) + (e / 3)) by A63, XREAL_1:8;
( f /. x10 = f . x10 & f /. x20 = f . x20 ) ;
hence ||.((f0 . x1) - (f0 . x2)).|| < e by A66, A64, XXREAL_0:2; :: thesis: verum

end;

end;

hence G is equicontinuous ; :: thesis: verum