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

proof

let r be Real; :: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (T . m),x0 < r )
reconsider V = Ball x0,r as Subset of (TopSpaceMetr Y) by TOPMETR:16;
assume r > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (T . m),x0 < r
then ( V is open & x0 in V ) by GOBOARD6:4, TOPMETR:21;
then consider W being Subset of (TopSpaceMetr X) such that
A5: ( p in W & W is open ) and
A6: f .: W c= V by A3, JGRAPH_2:20;
consider r0 being real number such that
A7: r0 > 0 and
A8: Ball (lim S),r0 c= W by A5, TOPMETR:22;
reconsider r00 = r0 as Real by XREAL_0:def 1;
consider n0 being Element of NAT such that
A9: for m being Element of NAT st n0 <= m holds
dist (S . m),(lim S) < r00 by A1, A7, TBSP_1:def 4;
for m being Element of NAT st n0 <= m holds
dist (T . m),x0 < r

proof

let m be Element of 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 A9;
then S . m in Ball (lim S),r0 by METRIC_1:12;
then A10: f . (S . m) in f .: W by A4, A8, FUNCT_1:def 12;
dom T = NAT by FUNCT_2:def 1;
then T . m in f .: W by A2, A10, FUNCT_1:22;
hence dist (T . m),x0 < r by A6, METRIC_1:12; :: thesis: verum

end;

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

end;

hence T is convergent by TBSP_1:def 3; :: thesis: verum