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

for r being Real

for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); :: thesis: ( f is continuous implies for r being Real

for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) ) )

assume A1: f is continuous ; :: thesis: for r being Real

for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

let r be Real; :: thesis: for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . 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 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

let u1 be Element of M; :: thesis: ( r > 0 & u1 = f . u implies ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) ) )

reconsider P = Ball (u1,r) as Subset of (TopSpaceMetr M) by TOPMETR:12;

A2: ( the carrier of N = the carrier of (TopSpaceMetr N) & dom f = the carrier of (TopSpaceMetr N) ) by FUNCT_2:def 1, TOPMETR:12;

assume ( r > 0 & u1 = f . u ) ; :: thesis: ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

then f . u in P by GOBOARD6:1;

then A3: u in f " P by A2, FUNCT_1:def 7;

f " P is open by A1, Th2;

then consider s1 being Real such that

A4: s1 > 0 and

A5: Ball (u,s1) c= f " P by A3, TOPMETR:15;

reconsider s1 = s1 as Real ;

for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s1 holds

dist (u1,w1) < r

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) ) by A4; :: thesis: verum

for r being Real

for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); :: thesis: ( f is continuous implies for r being Real

for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) ) )

assume A1: f is continuous ; :: thesis: for r being Real

for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

let r be Real; :: thesis: for u being Element of N

for u1 being Element of M st r > 0 & u1 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . 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 = f . u holds

ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

let u1 be Element of M; :: thesis: ( r > 0 & u1 = f . u implies ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) ) )

reconsider P = Ball (u1,r) as Subset of (TopSpaceMetr M) by TOPMETR:12;

A2: ( the carrier of N = the carrier of (TopSpaceMetr N) & dom f = the carrier of (TopSpaceMetr N) ) by FUNCT_2:def 1, TOPMETR:12;

assume ( r > 0 & u1 = f . u ) ; :: thesis: ex s being Real st

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) )

then f . u in P by GOBOARD6:1;

then A3: u in f " P by A2, FUNCT_1:def 7;

f " P is open by A1, Th2;

then consider s1 being Real such that

A4: s1 > 0 and

A5: Ball (u,s1) c= f " P by A3, TOPMETR:15;

reconsider s1 = s1 as Real ;

for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s1 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 = f . w & dist (u,w) < s1 holds

dist (u1,w1) < r

let w1 be Element of M; :: thesis: ( w1 = f . w & dist (u,w) < s1 implies dist (u1,w1) < r )

assume that

A6: w1 = f . w and

A7: dist (u,w) < s1 ; :: thesis: dist (u1,w1) < r

w in Ball (u,s1) by A7, METRIC_1:11;

then f . w in P by A5, FUNCT_1:def 7;

hence dist (u1,w1) < r by A6, METRIC_1:11; :: thesis: verum

end;dist (u1,w1) < r

let w1 be Element of M; :: thesis: ( w1 = f . w & dist (u,w) < s1 implies dist (u1,w1) < r )

assume that

A6: w1 = f . w and

A7: dist (u,w) < s1 ; :: thesis: dist (u1,w1) < r

w in Ball (u,s1) by A7, METRIC_1:11;

then f . w in P by A5, FUNCT_1:def 7;

hence dist (u1,w1) < r by A6, METRIC_1:11; :: thesis: verum

( s > 0 & ( for w being Element of N

for w1 being Element of M st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r ) ) by A4; :: thesis: verum