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
for u being Element of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being Real 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; :: thesis: for u being Element of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being Real 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 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 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 ;
assume that
A3: r > 0 and
A4: u1 = g . u ; :: thesis: ex s being Real 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)) < r by A2, A3;
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 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 Th3; :: thesis: verum