let N, M be non empty MetrSpace; :: thesis:
let f be Function of N,M; :: thesis:
let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); :: thesis:
assume A1: ( g = f & TopSpaceMetr N is compact & g is continuous ) ; :: thesis:
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist u1,u2 < s holds
dist (f /. u1),(f /. u2) < r ) )

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then A2: 0 < r / 2 by XREAL_1:217;
set G = { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } ;
A3: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:16;
{ P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } c= bool the carrier of N

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } ; :: thesis:
then consider P being Subset of (TopSpaceMetr N) such that
A4: ( x = P & ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) ) ;
thus x in bool the carrier of N by A4; :: thesis:

end;

then reconsider G1 = { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } as Subset-Family of (TopSpaceMetr N) by TOPMETR:16;
the carrier of N c= union G1

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of N ; :: thesis:
then reconsider w0 = x as Element of N ;
g . w0 = f /. w0 by A1;
then reconsider w4 = g . w0 as Element of M ;
consider s4 being Real such that
A5: s4 > 0 and
A6: for u5 being Element of N
for w5 being Element of M st w5 = g . u5 & dist w0,u5 < s4 holds
dist w4,w5 < r / 2 by A1, A2, Th5;
A7: x in Ball w0,s4 by A5, GOBOARD6:4;
reconsider P2 = Ball w0,s4 as Subset of (TopSpaceMetr N) by TOPMETR:16;
for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w0 & w3 = f . w1 & dist w0,w1 < s4 holds
dist w2,w3 < r / 2 by A1, A6;
then ex w being Element of N ex s being Real st
( P2 = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) ;
then Ball w0,s4 in G1 ;
hence x in union G1 by A7, TARSKI:def 4; :: thesis:

end;

then A8: the carrier of N = union G1 by A3, XBOOLE_0:def 10;
the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:16;
then A9: G1 is Cover of (TopSpaceMetr N) by A8, SETFAM_1:60;
for P3 being Subset of (TopSpaceMetr N) st P3 in G1 holds
P3 is open

let P3 be Subset of (TopSpaceMetr N); :: thesis:
assume P3 in G1 ; :: thesis:
then consider P being Subset of (TopSpaceMetr N) such that
A10: P3 = P and
A11: ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) ;
consider w being Element of N, s being Real such that
A12: P = Ball w,s and
for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 by A11;
thus P3 is open by A10, A12, TOPMETR:21; :: thesis:

end;

then G1 is open by TOPS_2:def 1;
then consider s1 being Real such that
A13: s1 > 0 and
A14: for w1, w2 being Element of N st dist w1,w2 < s1 holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G1 ) by A1, A9, Th7;
for u1, u2 being Element of N st dist u1,u2 < s1 holds
dist (f /. u1),(f /. u2) < r

let u1, u2 be Element of N; :: thesis:
assume dist u1,u2 < s1 ; :: thesis:
then consider Ga being Subset of (TopSpaceMetr N) such that
A15: ( u1 in Ga & u2 in Ga & Ga in G1 ) by A14;
consider P being Subset of (TopSpaceMetr N) such that
A16: ( Ga = P & ex w being Element of N ex s2 being Real st
( P = Ball w,s2 & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s2 holds
dist w2,w3 < r / 2 ) ) ) by A15;
consider w being Element of N, s2 being Real such that
A17: ( P = Ball w,s2 & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s2 holds
dist w2,w3 < r / 2 ) ) by A16;
A18: dist w,u1 < s2 by A15, A16, A17, METRIC_1:12;
A19: dist w,u2 < s2 by A15, A16, A17, METRIC_1:12;
A20: dist (f /. w),(f /. u1) < r / 2 by A17, A18;
A21: dist (f /. w),(f /. u2) < r / 2 by A17, A19;
A22: dist (f /. u1),(f /. u2) <= (dist (f /. u1),(f /. w)) + (dist (f /. w),(f /. u2)) by METRIC_1:4;
(dist (f /. w),(f /. u1)) + (dist (f /. w),(f /. u2)) < (r / 2) + (r / 2) by A20, A21, XREAL_1:10;
hence dist (f /. u1),(f /. u2) < r by A22, XXREAL_0:2; :: thesis:

end;

hence ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist u1,u2 < s holds
dist (f /. u1),(f /. u2) < r ) ) by A13; :: thesis:

end;

hence f is uniformly_continuous by Def1; :: thesis: