let S be non empty MetrSpace; :: thesis:
let V be non empty compact TopSpace; :: thesis:
let T be NormedLinearTopSpace; :: thesis:
let f be Function of V,T; :: thesis:
assume A1: V = TopSpaceMetr S ; :: thesis:

hereby :: thesis:

assume A2: f is continuous ; :: thesis:
let e be Real; :: thesis:
assume A3: 0 < e ; :: thesis:
A4: [#] (TopSpaceMetr S) is compact by A1, COMPTS_1:1;
defpred S₁[ Element of S, Real] means ( 0 < $2 & ( for x being Point of S st dist (x,$1) < $2 holds
||.((f /. x) - (f /. $1)).|| < e / 2 ) );
A5: 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:
reconsider xx0 = x0 as Point of V by A1;
consider H being Subset of V such that
A6: ( H is open & xx0 in H & ( for y being Point of V st y in H holds
||.((f . xx0) - (f . y)).|| < e / 2 ) ) by A3, Th3, A2, TMAP_1:50;
consider d being Real such that
A7: ( d > 0 & Ball (x0,d) c= H ) by A1, PCOMPS_1:def 4, A6;
reconsider d = d as Element of REAL by XREAL_0:def 1;
take d ; :: thesis:
for x being Point of S st dist (x,x0) < d holds
||.((f /. x) - (f /. x0)).|| < e / 2

proof

let x be Point of S; :: thesis:
assume dist (x,x0) < d ; :: thesis:
then x in { y where y is Point of S : dist (x0,y) < d } ;
then A8: x in Ball (x0,d) by METRIC_1:def 14;
reconsider y = x as Point of V by A1;
A9: ||.((f . xx0) - (f . y)).|| < e / 2 by A6, A8, A7;
( f . xx0 = f /. xx0 & f . y = f /. y ) ;
hence ||.((f /. x) - (f /. x0)).|| < e / 2 by A9, NORMSP_1:7; :: thesis:

end;

hence S₁[x0,d] by A7; :: 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(A5);
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 ;
0 < (D . x0) / 2 by A10, XREAL_1:215;
then dist (x0,x0) < (D . x0) / 2 by 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, A4, 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;
set d0 = lower_bound D0;
A28: for r being Real st r in D0 holds
lower_bound D0 <= r by SEQ_4:def 2;
lower_bound D0 in D0 by SEQ_4:133, A27;
then 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;
reconsider xx = xx as Point of S by A29;
A30: 0 < lower_bound D0 by A29, A10;
reconsider d = (lower_bound D0) / 2 as Real ;
take d = d; :: thesis:
thus 0 < d by A30; :: thesis:
thus for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < e :: thesis:

proof

let x1, x2 be Point of S; :: thesis:
assume A31: 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
A32: ( x1 in X1 & X1 in G ) by TARSKI:def 4;
A33: X1 = Ball ((H /. X1),((D . (H . X1)) / 2)) by A21, 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 A24, PARTFUN1:def 6, A32;
then dist (x1,(H /. X1)) < D . (H /. X1) by A34, XXREAL_0:2;
then A36: ||.((f /. x1) - (f /. (H /. X1))).|| < e / 2 by A10;
A37: H . X1 in rng H by A24, A32, FUNCT_1:3;
H /. X1 in dom D by A25;
then H . X1 in dom D by A24, A32, PARTFUN1:def 6;
then D . (H . X1) in D0 by FUNCT_1:def 6, A37;
then (lower_bound D0) / 2 <= (D . (H . X1)) / 2 by A28, 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 A40: dist (x2,(H /. X1)) < D . (H . X1) by A39, XXREAL_0:2;
dist (x2,(H /. X1)) < D . (H /. X1) by PARTFUN1:def 6, A24, A40, A32;
then A41: ||.((f /. x2) - (f /. (H /. X1))).|| < e / 2 by A10;
(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 A42: ||.((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 A41, A36, XREAL_1:8;
hence ||.((f /. x1) - (f /. x2)).|| < e by A42, XXREAL_0:2; :: thesis:

end;

assume A43: for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < e ) ) ; :: thesis:
for x being Point of V holds f is_continuous_at x

proof

let x be Point of V; :: thesis:

now :: thesis:

let e be Real; :: thesis:
assume A44: 0 < e ; :: thesis:
reconsider x0 = x as Point of S by A1;
consider d being Real such that
A45: ( 0 < d & ( for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < e ) ) by A44, A43;
reconsider H = Ball (x0,d) as Subset of V by A1;
take H = H; :: thesis:
thus H is open by A1, PCOMPS_1:29; :: thesis:
dist (x0,x0) < d by A45, METRIC_1:1;
hence x in H by METRIC_1:11; :: thesis:
thus for y being Point of V st y in H holds
||.((f . x) - (f . y)).|| < e :: thesis:

proof

let y be Point of V; :: thesis:
assume y in H ; :: thesis:
then y in { t where t is Point of S : dist (x0,t) < d } by METRIC_1:def 14;
then A46: ex t being Point of S st
( y = t & dist (x0,t) < d ) ;
reconsider y0 = y as Point of S by A1;
dom f = the carrier of S by A1, FUNCT_2:def 1;
then ( f /. x0 = f . x0 & f /. y0 = f . y0 ) by PARTFUN1:def 6;
hence ||.((f . x) - (f . y)).|| < e by A45, A46; :: thesis:

end;

hence f is_continuous_at x by Th3; :: thesis:

end;

hence f is continuous by TMAP_1:50; :: thesis: