let S, T be non empty MetrSpace; :: thesis:
let f be Function of (TopSpaceMetr S),(TopSpaceMetr T); :: thesis:
assume A1: TopSpaceMetr S is compact ; :: thesis:
set V = TopSpaceMetr S;

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
dist ((In ((f /. x),T)),(In ((f /. $1),T))) < 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 (TopSpaceMetr S) ;
consider H being Subset of (TopSpaceMetr S) such that
A6: ( H is open & xx0 in H & ( for y being Point of (TopSpaceMetr S) st y in H holds
dist ((In ((f . xx0),T)),(In ((f . y),T))) < e / 2 ) ) by A3, Th2, A2, TMAP_1:50;
consider d being Real such that
A7: ( d > 0 & Ball (x0,d) c= H ) by 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
dist ((In ((f /. x),T)),(In ((f /. x0),T))) < e / 2

proof

let x be Point of S; :: thesis:
assume dist (x,x0) < d ; :: thesis:
then A8: x in Ball (x0,d) by METRIC_1:11;
reconsider y = x as Point of (TopSpaceMetr S) ;
A9: dist ((In ((f . xx0),T)),(In ((f . y),T))) < e / 2 by A6, A8, A7;
( f . xx0 = f /. xx0 & f . y = f /. y ) ;
hence dist ((In ((f /. x),T)),(In ((f /. x0),T))) < e / 2 by A9; :: 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
A15: ( 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)) );
A16: 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 A15;
then consider x0 being Point of S such that
A17: Z = Ball (x0,((D . x0) / 2)) ;
take x0 ; :: thesis:
thus ( x0 in the carrier of S & S₂[Z,x0] ) by A17; :: thesis:

end;

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

proof

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

end;

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

end;

then consider xx being object such that
A24: xx in G by XBOOLE_0:def 1;
rng H <> {} by A22, A24, FUNCT_1:3;
then consider xx being object such that
A25: xx in rng H by XBOOLE_0:def 1;
reconsider xx = xx as Point of S by A25;
set d0 = lower_bound D0;
A26: 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, A25;
then consider xx being object such that
A27: ( 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 A27;
A28: 0 < lower_bound D0 by A27, A10;
reconsider d = (lower_bound D0) / 2 as Real ;
take d = d; :: thesis:
thus 0 < d by A28; :: thesis:
thus for x1, x2 being Point of S st dist (x1,x2) < d holds
dist ((In ((f /. x1),T)),(In ((f /. x2),T))) < e :: thesis:

proof

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

end;

assume A41: 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
dist ((In ((f /. x1),T)),(In ((f /. x2),T))) < e ) ) ; :: thesis:
for x being Point of (TopSpaceMetr S) holds f is_continuous_at x

proof

let x be Point of (TopSpaceMetr S); :: thesis:

now :: thesis:

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

proof

let y be Point of (TopSpaceMetr S); :: 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 A44: ex t being Point of S st
( y = t & dist (x0,t) < d ) ;
reconsider y0 = y as Point of S ;
dom f = the carrier of S by FUNCT_2:def 1;
then ( f /. x0 = f . x0 & f /. y0 = f . y0 ) by PARTFUN1:def 6;
hence dist ((In ((f . x),T)),(In ((f . y),T))) < e by A43, A44; :: thesis:

end;

hence f is_continuous_at x by Th2; :: thesis:

end;

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