let S, T be non empty MetrSpace; :: 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 ASCOLI2:def 2 :: 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
dist ((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 dist ((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 ASCOLI2:def 3 :: 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
dist ((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
dist ((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 Ball (x0,((D . x0) / 2)) by METRIC_1:11;
hence z in union CV by TARSKI:def 4, A14; :: thesis:

end;

then consider G being Subset-Family of (TopSpaceMetr S) such that
A16: ( 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)) );
A17: 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 A16;
then consider x0 being Point of S such that
A18: Z = Ball (x0,((D . x0) / 2)) ;
take x0 ; :: thesis:
thus ( x0 in the carrier of S & S₂[Z,x0] ) by A18; :: thesis:

end;

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

proof

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

end;

A23: dom H = G by FUNCT_2:def 1;
reconsider D0 = D .: (rng H) as finite Subset of REAL by A16;
A24: 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, A16, SETFAM_1:def 11;
hence contradiction ; :: thesis:

end;

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

proof

let f be Function of S,T; :: thesis:
assume A30: f in F ; :: thesis:
let x1, x2 be Point of S; :: thesis:
assume A31: dist (x1,x2) < d ; :: thesis:
x1 in union G by A16, SETFAM_1:def 11, TARSKI:def 3;
then consider X1 being set such that
A32: ( x1 in X1 & X1 in G ) by TARSKI:def 4;
A33: X1 = Ball ((H /. X1),((D . (H . X1)) / 2)) by A20, A32;
A34: (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 A33, A32, METRIC_1:def 14;
then A35: 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 A23, PARTFUN1:def 6, A32;
then dist (x1,(H /. X1)) < D . (H /. X1) by A34, XXREAL_0:2;
then A36: dist ((f . x1),(f . (H /. X1))) < e / 2 by A10, A30;
A37: H . X1 in rng H by A23, A32, FUNCT_1:3;
H /. X1 in dom D by A24;
then H . X1 in dom D by A23, A32, PARTFUN1:def 6;
then D . (H . X1) in D0 by FUNCT_1:def 6, A37;
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 A38: dist (x1,x2) < (D . (H . X1)) / 2 by A31, XXREAL_0:2;
A39: 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 A38, A35, XREAL_1:8;
then dist (x2,(H /. X1)) < D . (H . X1) by A39, XXREAL_0:2;
then dist (x2,(H /. X1)) < D . (H /. X1) by PARTFUN1:def 6, A23, A32;
then A40: dist ((f . x2),(f . (H /. X1))) < e / 2 by A10, A30;
A41: dist ((f . x1),(f . x2)) <= (dist ((f . x1),(f . (H /. X1)))) + (dist ((f . x2),(f . (H /. X1)))) by METRIC_1:4;
(dist ((f . x1),(f . (H /. X1)))) + (dist ((f . x2),(f . (H /. X1)))) < (e / 2) + (e / 2) by A40, A36, XREAL_1:8;
hence dist ((f . x1),(f . x2)) < e by A41, XXREAL_0:2; :: thesis:

end;