let X, Y be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y) holds
( f is continuous iff for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S holds
( T is convergent & lim T = f . (lim S) ) )
let f be Function of (TopSpaceMetr X),(TopSpaceMetr Y); :: thesis: ( f is continuous iff for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S holds
( T is convergent & lim T = f . (lim S) ) )

hereby :: thesis: ( ( for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S holds
( T is convergent & lim T = f . (lim S) ) ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S holds
( T is convergent & lim T = f . (lim S) )
let S be sequence of X; :: thesis: for T being sequence of Y st S is convergent & T = f * S holds
( T is convergent & lim T = f . (lim S) )
let T be sequence of Y; :: thesis: ( S is convergent & T = f * S implies ( T is convergent & lim T = f . (lim S) ) )
assume that
A2: S is convergent and
A3: T = f * S ; :: thesis: ( T is convergent & lim T = f . (lim S) )
set z0 = lim S;
reconsider p = lim S as Point of (TopSpaceMetr X) ;
A4: dom f = the carrier of X by FUNCT_2:def 1;
then f . (lim S) in rng f by FUNCT_1:3;
then reconsider x0 = f . (lim S) as Element of Y ;
A5: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r

proof

let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r )
reconsider V = Ball (x0,r) as Subset of (TopSpaceMetr Y) ;
assume r > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r
then ( V is open & x0 in V ) by GOBOARD6:1, TOPMETR:14;
then consider W being Subset of (TopSpaceMetr X) such that
A6: ( p in W & W is open ) and
A7: f .: W c= V by A1, JGRAPH_2:10;
consider r0 being Real such that
A8: r0 > 0 and
A9: Ball ((lim S),r0) c= W by A6, TOPMETR:15;
reconsider r00 = r0 as Real ;
consider n0 being Nat such that
A10: for m being Nat st n0 <= m holds
dist ((S . m),(lim S)) < r00 by A2, A8, TBSP_1:def 3;
for m being Nat st n0 <= m holds
dist ((T . m),x0) < r

proof

let m be Nat; :: thesis: ( n0 <= m implies dist ((T . m),x0) < r )
assume n0 <= m ; :: thesis: dist ((T . m),x0) < r
then dist ((S . m),(lim S)) < r0 by A10;
then S . m in Ball ((lim S),r0) by METRIC_1:11;
then A11: f . (S . m) in f .: W by A4, A9, FUNCT_1:def 6;
dom T = NAT by FUNCT_2:def 1;
then T . m in f .: W by A3, A11, FUNCT_1:12, ORDINAL1:def 12;
hence dist ((T . m),x0) < r by A7, METRIC_1:11; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r ; :: thesis: verum

end;

hence T is convergent ; :: thesis: lim T = f . (lim S)
hence lim T = f . (lim S) by A5, TBSP_1:def 3; :: thesis: verum

end;

assume A12: for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S holds
( T is convergent & lim T = f . (lim S) ) ; :: thesis: f is continuous
for B being Subset of (TopSpaceMetr Y) st B is closed holds
f " B is closed

proof

let B be Subset of (TopSpaceMetr Y); :: thesis: ( B is closed implies f " B is closed )
reconsider A = f " B as Subset of (TopSpaceMetr X) ;
assume A13: B is closed ; :: thesis: f " B is closed
for S being sequence of X st ( for n being Nat holds S . n in f " B ) & S is convergent holds
lim S in f " B

proof

let S be sequence of X; :: thesis: ( ( for n being Nat holds S . n in f " B ) & S is convergent implies lim S in f " B )
assume that
A14: for n being Nat holds S . n in f " B and
A15: S is convergent ; :: thesis: lim S in f " B
reconsider T = f * S as sequence of Y ;
for n being Nat holds T . n in B

proof

let n be Nat; :: thesis: T . n in B
S . n in f " B by A14;
then f . (S . n) in B by FUNCT_1:def 7;
hence T . n in B by FUNCT_2:15, ORDINAL1:def 12; :: thesis: verum

end;

then lim T in B by A12, A13, A15, Th4;
then A16: f . (lim S) in B by A12, A15;
dom f = the carrier of X by FUNCT_2:def 1;
hence lim S in f " B by A16, FUNCT_1:def 7; :: thesis: verum

end;

hence f " B is closed by Th4; :: thesis: verum

end;

hence f is continuous ; :: thesis: verum