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 that
A1: f = g and
A2: f is uniformly_continuous ; :: thesis: g is continuous
for r being real number
for u being Element 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 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 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 r9 = r as Real by XREAL_0:def 1;
assume that
A3: r > 0 and
A4: 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 ) )
consider s being Real such that
A5: 0 < s and
A6: for wu1, wu2 being Element of N st dist wu1,wu2 < s holds
dist (f /. wu1),(f /. wu2) < r9 by A2, A3, 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 that
A7: w1 = g . w and
A8: dist u,w < s ; :: thesis: dist u1,w1 < r
A9: u1 = f /. u by A1, A4;
w1 = f /. w by A1, A7;
hence dist u1,w1 < r by A6, A8, A9; :: 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 A5; :: thesis: verum

end;

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