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 ) )

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

hence
g is continuous
by Th3; :: thesis: verum
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

( 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;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

hence
ex s being Real st
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;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

( 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