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:16;
A2: ( the carrier of N = the carrier of (TopSpaceMetr N) & dom f = the carrier of (TopSpaceMetr N) ) by FUNCT_2:def 1, TOPMETR:16;
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:4;
then A3: u in f " P by A2, FUNCT_1:def 13;
f " P is open by A1, Th3;
then consider s1 being real number such that
A4: s1 > 0 and
A5: Ball u,s1 c= f " P by A3, TOPMETR:22;
reconsider s1 = s1 as Real by XREAL_0:def 1;
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 A7, METRIC_1:12;
then f . w in P by A5, FUNCT_1:def 13;
hence dist u1,w1 < r by A6, METRIC_1:12; :: 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