let S be non empty MetrSpace; :: thesis:
let T be RealNormSpace; :: thesis:
let F be Subset of (Funcs ( the carrier of S, the carrier of T)); :: thesis:
assume A1: TopSpaceMetr S is compact ; :: thesis:

hereby :: thesis:

assume A2: F is equicontinuous ; :: thesis:
thus for x being Point of S holds F is_equicontinuous_at x :: thesis:

proof

let x0 be Point of S; :: thesis:
let e be Real; :: according to ASCOLI:def 3 :: thesis:
assume 0 < e ; :: thesis:
then consider d being Real such that
A3: ( 0 < d & ( for f being Function of the carrier of S, the carrier of T st f in F holds
for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) ) by A2;
take d ; :: thesis:
thus 0 < d by A3; :: thesis:
let f be Function of the carrier of S, the carrier of T; :: thesis:
assume A4: f in F ; :: thesis:
let x be Point of S; :: thesis:
assume dist (x,x0) < d ; :: thesis:
hence ||.((f . x) - (f . x0)).|| < e by A3, A4; :: thesis:

end;

assume A5: for x being Point of S holds F is_equicontinuous_at x ; :: thesis:
let e be Real; :: according to ASCOLI:def 4 :: thesis:
assume A6: 0 < e ; :: thesis:
A7: [#] (TopSpaceMetr S) is compact by A1, COMPTS_1:1;
defpred S₁[ Element of S, Real] means ( 0 < $2 & ( for f being Function of the carrier of S, the carrier of T st f in F holds
for x being Point of S st dist (x,$1) < $2 holds
||.((f . x) - (f . $1)).|| < e / 2 ) );
A8: for x0 being Element of the carrier of S ex d being Element of REAL st S₁[x0,d]

proof

let x0 be Element of the carrier of S; :: thesis:
F is_equicontinuous_at x0 by A5;
then consider d being Real such that
A9: ( 0 < d & ( for f being Function of the carrier of S, the carrier of T st f in F holds
for x being Point of S st dist (x,x0) < d holds
||.((f . x) - (f . x0)).|| < e / 2 ) ) by A6;
reconsider d = d as Element of REAL by XREAL_0:def 1;
take d ; :: thesis:
thus S₁[x0,d] by A9; :: thesis:

end;

consider D being Function of the carrier of S,REAL such that
A10: for x0 being Element of the carrier of S holds S₁[x0,D . x0] from FUNCT_2:sch 3(A8);
set CV = { (Ball (x0,((D . x0) / 2))) where x0 is Element of S : verum } ;
{ (Ball (x0,((D . x0) / 2))) where x0 is Element of S : verum } c= bool the carrier of (TopSpaceMetr S)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { (Ball (x0,((D . x0) / 2))) where x0 is Element of S : verum } ; :: thesis:
then consider x0 being Point of S such that
A11: z = Ball (x0,((D . x0) / 2)) ;
thus z in bool the carrier of (TopSpaceMetr S) by A11; :: thesis:

end;

then reconsider CV = { (Ball (x0,((D . x0) / 2))) where x0 is Element of S : verum } as Subset-Family of (TopSpaceMetr S) ;
for P being Subset of (TopSpaceMetr S) st P in CV holds
P is open

proof

let P be Subset of (TopSpaceMetr S); :: thesis:
assume P in CV ; :: thesis:
then consider x0 being Point of S such that
A12: P = Ball (x0,((D . x0) / 2)) ;
thus P is open by A12, PCOMPS_1:29; :: thesis:

end;

then A13: CV is open by TOPS_2:def 1;
the carrier of (TopSpaceMetr S) c= union CV

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in the carrier of (TopSpaceMetr S) ; :: thesis:
then reconsider x0 = z as Point of S ;
A14: Ball (x0,((D . x0) / 2)) in CV ;
A15: 0 < (D . x0) / 2 by A10, XREAL_1:215;
dist (x0,x0) < (D . x0) / 2 by A15, METRIC_1:1;
then x0 in { y where y is Element of S : dist (x0,y) < (D . x0) / 2 } ;
then x0 in Ball (x0,((D . x0) / 2)) by METRIC_1:def 14;
hence z in union CV by TARSKI:def 4, A14; :: thesis:

end;

then consider G being Subset-Family of (TopSpaceMetr S) such that
A17: ( G c= CV & G is Cover of [#] (TopSpaceMetr S) & G is finite ) by COMPTS_1:def 4, A7, A13, SETFAM_1:def 11;
defpred S₂[ object , object ] means ex x0 being Point of S st
( $2 = x0 & $1 = Ball (x0,((D . x0) / 2)) );
A18: for Z being object st Z in G holds
ex x0 being object st
( x0 in the carrier of S & S₂[Z,x0] )

proof

let Z be object ; :: thesis:
assume Z in G ; :: thesis:
then Z in CV by A17;
then consider x0 being Point of S such that
A19: Z = Ball (x0,((D . x0) / 2)) ;
take x0 ; :: thesis:
thus ( x0 in the carrier of S & S₂[Z,x0] ) by A19; :: thesis:

end;

consider H being Function of G, the carrier of S such that
A20: for Z being object st Z in G holds
S₂[Z,H . Z] from FUNCT_2:sch 1(A18);
A21: for Z being object st Z in G holds
Z = Ball ((H /. Z),((D . (H . Z)) / 2))

proof

let Z be object ; :: thesis:
assume A22: Z in G ; :: thesis:
then A23: ex x0 being Point of S st
( H . Z = x0 & Z = Ball (x0,((D . x0) / 2)) ) by A20;
dom H = G by FUNCT_2:def 1;
hence Z = Ball ((H /. Z),((D . (H . Z)) / 2)) by A23, A22, PARTFUN1:def 6; :: thesis:

end;

A24: dom H = G by FUNCT_2:def 1;
reconsider D0 = D .: (rng H) as finite Subset of REAL by A17;
A25: dom D = the carrier of S by FUNCT_2:def 1;
G <> {}

proof

assume G = {} ; :: thesis:
then the carrier of (TopSpaceMetr S) c= {} by ZFMISC_1:2, A17, SETFAM_1:def 11;
hence contradiction ; :: thesis:

end;

then consider xx being object such that
A26: xx in G by XBOOLE_0:def 1;
rng H <> {} by A24, A26, FUNCT_1:3;
then consider xx being object such that
A27: xx in rng H by XBOOLE_0:def 1;
reconsider xx = xx as Point of S by A27;
A28: ( D0 is bounded_below & lower_bound D0 in D0 ) by SEQ_4:133, A27;
set d0 = lower_bound D0;
consider xx being object such that
A29: ( xx in dom D & xx in rng H & lower_bound D0 = D . xx ) by FUNCT_1:def 6, A28;
reconsider xx = xx as Point of S by A29;
A30: 0 < lower_bound D0 by A29, A10;
take d = (lower_bound D0) / 2; :: thesis:
thus 0 < d by A30; :: thesis:
thus for f being Function of S,T st f in F holds
for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e :: thesis:

proof

let f be Function of S,T; :: thesis:
assume A31: f in F ; :: thesis:
let x1, x2 be Point of S; :: thesis:
assume A32: dist (x1,x2) < d ; :: thesis:
x1 in union G by A17, SETFAM_1:def 11, TARSKI:def 3;
then consider X1 being set such that
A33: ( x1 in X1 & X1 in G ) by TARSKI:def 4;
A34: X1 = Ball ((H /. X1),((D . (H . X1)) / 2)) by A21, A33;
A35: (D . (H /. X1)) / 2 < D . (H /. X1) by A10, XREAL_1:216;
x1 in { y where y is Point of S : dist ((H /. X1),y) < (D . (H . X1)) / 2 } by A34, A33, METRIC_1:def 14;
then A36: ex y being Point of S st
( y = x1 & dist ((H /. X1),y) < (D . (H . X1)) / 2 ) ;
then dist (x1,(H /. X1)) < (D . (H /. X1)) / 2 by A24, PARTFUN1:def 6, A33;
then dist (x1,(H /. X1)) < D . (H /. X1) by A35, XXREAL_0:2;
then A37: ||.((f . x1) - (f . (H /. X1))).|| < e / 2 by A10, A31;
A38: H . X1 in rng H by A24, A33, FUNCT_1:3;
H /. X1 in dom D by A25;
then H . X1 in dom D by A24, A33, PARTFUN1:def 6;
then D . (H . X1) in D0 by FUNCT_1:def 6, A38;
then lower_bound D0 <= D . (H . X1) by SEQ_4:def 2;
then (lower_bound D0) / 2 <= (D . (H . X1)) / 2 by XREAL_1:72;
then A39: dist (x1,x2) < (D . (H . X1)) / 2 by A32, XXREAL_0:2;
A40: dist (x2,(H /. X1)) <= (dist (x1,x2)) + (dist ((H /. X1),x1)) by METRIC_1:4;
(dist (x1,x2)) + (dist ((H /. X1),x1)) < ((D . (H . X1)) / 2) + ((D . (H . X1)) / 2) by A39, A36, XREAL_1:8;
then dist (x2,(H /. X1)) < D . (H . X1) by A40, XXREAL_0:2;
then dist (x2,(H /. X1)) < D . (H /. X1) by PARTFUN1:def 6, A24, A33;
then A42: ||.((f . x2) - (f . (H /. X1))).|| < e / 2 by A10, A31;
(f . x1) - (f . x2) = (((f . x1) - (f . (H /. X1))) + (f . (H /. X1))) - (f . x2) by RLVECT_4:1
.= ((f . x1) - (f . (H /. X1))) + ((f . (H /. X1)) - (f . x2)) by RLVECT_1:28 ;
then ||.((f . x1) - (f . x2)).|| <= ||.((f . x1) - (f . (H /. X1))).|| + ||.((f . (H /. X1)) - (f . x2)).|| by NORMSP_1:def 1;
then A43: ||.((f . x1) - (f . x2)).|| <= ||.((f . x1) - (f . (H /. X1))).|| + ||.((f . x2) - (f . (H /. X1))).|| by NORMSP_1:7;
||.((f . x1) - (f . (H /. X1))).|| + ||.((f . x2) - (f . (H /. X1))).|| < (e / 2) + (e / 2) by A42, A37, XREAL_1:8;
hence ||.((f . x1) - (f . x2)).|| < e by A43, XXREAL_0:2; :: thesis:

end;