let N, M be non empty MetrSpace; :: thesis: for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous
let f be Function of N,M; :: thesis: for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous
let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); :: thesis: ( f = g & f is uniformly_continuous implies g is continuous )
assume A1: ( f = g & f is uniformly_continuous ) ; :: thesis: g is continuous
for r being real number
for u being Element of the carrier of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r ) )

proof

let r be real number ; :: thesis: for u being Element of the carrier of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r ) )
let u be Element of the carrier of N; :: thesis: for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r ) )
let u1 be Element of M; :: thesis: ( r > 0 & u1 = g . u implies ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r ) ) )
reconsider r' = r as Real by XREAL_0:def 1;
assume A2: ( r > 0 & u1 = g . u ) ; :: thesis: ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r ) )
then consider s being Real such that
A3: ( 0 < s & ( for wu1, wu2 being Element of N st dist wu1,wu2 < s holds
dist (f /. wu1),(f /. wu2) < r' ) ) by A1, Def1;
for w being Element of N
for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r

proof

let w be Element of N; :: thesis: for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r
let w1 be Element of M; :: thesis: ( w1 = g . w & dist u,w < s implies dist u1,w1 < r )
assume A4: ( w1 = g . w & dist u,w < s ) ; :: thesis: dist u1,w1 < r
A5: u1 = f /. u by A1, A2;
w1 = f /. w by A1, A4;
hence dist u1,w1 < r by A3, A4, A5; :: thesis: verum

end;

hence ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist u,w < s holds
dist u1,w1 < r ) ) by A3; :: thesis: verum

end;

hence g is continuous by Th4; :: thesis: verum