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