let N, M be non empty MetrSpace; :: thesis: for f being Function of (),() 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 (),(); :: 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 () by TOPMETR:12;
A2: ( the carrier of N = the carrier of () & dom f = the carrier of () ) by ;
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 ;
f " P is open by ;
then consider s1 being Real such that
A4: s1 > 0 and
A5: Ball (u,s1) c= f " P by ;
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
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 ;
then f . w in P by ;
hence dist (u1,w1) < r by ; :: 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 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) by A4; :: thesis: verum