let N, M be non empty MetrSpace; :: thesis: for f being Function of N,M
for g being Function of (),() st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous

let f be Function of N,M; :: thesis: for g being Function of (),() st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous

let g be Function of (),(); :: thesis: ( g = f & TopSpaceMetr N is compact & g is continuous implies f is uniformly_continuous )
assume that
A1: g = f and
A2: TopSpaceMetr N is compact and
A3: 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 ) )
proof
let r be Real; :: thesis: ( 0 < r implies 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 ) ) )

set G = { P where P is Subset of () : 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 ) )
}
;
A4: the carrier of () = the carrier of N by TOPMETR:12;
{ P where P is Subset of () : 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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { P where P is Subset of () : 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 ) )
}
or x in bool the carrier of N )

assume x in { P where P is Subset of () : 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: x in bool the carrier of N
then ex P being Subset of () st
( 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 ) ) ) ;
hence x in bool the carrier of N ; :: thesis: verum
end;
then reconsider G1 = { P where P is Subset of () : 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 () by TOPMETR:12;
for P3 being Subset of () st P3 in G1 holds
P3 is open
proof
let P3 be Subset of (); :: thesis: ( P3 in G1 implies P3 is open )
assume P3 in G1 ; :: thesis: P3 is open
then ex P being Subset of () st
( P3 = 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 ) ) ) ;
hence P3 is open by TOPMETR:14; :: thesis: verum
end;
then A5: G1 is open by TOPS_2:def 1;
assume 0 < r ; :: thesis: 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 ) )

then A6: 0 < r / 2 by XREAL_1:215;
A7: the carrier of N c= union G1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of N or x in union G1 )
assume x in the carrier of N ; :: thesis: x in union G1
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
A8: s4 > 0 and
A9: 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 A3, A6, Th4;
reconsider P2 = Ball (w0,s4) as Subset of () by TOPMETR:12;
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, A9;
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 A10: Ball (w0,s4) in G1 ;
x in Ball (w0,s4) by ;
hence x in union G1 by ; :: thesis: verum
end;
the carrier of () = the carrier of N by TOPMETR:12;
then the carrier of N = union G1 by ;
then G1 is Cover of () by ;
then consider s1 being Real such that
A11: s1 > 0 and
A12: for w1, w2 being Element of N st dist (w1,w2) < s1 holds
ex Ga being Subset of () st
( w1 in Ga & w2 in Ga & Ga in G1 ) by A2, A5, Th6;
for u1, u2 being Element of N st dist (u1,u2) < s1 holds
dist ((f /. u1),(f /. u2)) < r
proof
let u1, u2 be Element of N; :: thesis: ( dist (u1,u2) < s1 implies dist ((f /. u1),(f /. u2)) < r )
assume dist (u1,u2) < s1 ; :: thesis: dist ((f /. u1),(f /. u2)) < r
then consider Ga being Subset of () such that
A13: u1 in Ga and
A14: u2 in Ga and
A15: Ga in G1 by A12;
consider P being Subset of () such that
A16: Ga = P and
A17: 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
A18: P = Ball (w,s2) and
A19: 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 A17;
dist (w,u2) < s2 by ;
then A20: dist ((f /. w),(f /. u2)) < r / 2 by A19;
dist (w,u1) < s2 by ;
then dist ((f /. w),(f /. u1)) < r / 2 by A19;
then ( dist ((f /. u1),(f /. u2)) <= (dist ((f /. u1),(f /. w))) + (dist ((f /. w),(f /. u2))) & (dist ((f /. w),(f /. u1))) + (dist ((f /. w),(f /. u2))) < (r / 2) + (r / 2) ) by ;
hence dist ((f /. u1),(f /. u2)) < r by XXREAL_0:2; :: thesis: verum
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 A11; :: thesis: verum
end;
hence f is uniformly_continuous ; :: thesis: verum