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 A1: ( S is convergent & T = f * S & f is continuous ) ; :: thesis: T is convergent
A2: 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;
set z0 = lim S;
reconsider p = lim S as Point of (TopSpaceMetr X) 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 )
assume A3: 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
reconsider V = Ball x0,r as Subset of (TopSpaceMetr Y) by TOPMETR:16;
A4: V is open by TOPMETR:21;
x0 in V by A3, GOBOARD6:4;
then consider W being Subset of (TopSpaceMetr X) such that
A5: ( p in W & W is open & f .: W c= V ) by A1, A4, JGRAPH_2:20;
consider r0 being real number such that
A6: ( r0 > 0 & 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
A7: for m being Element of NAT st n0 <= m holds
dist (S . m),(lim S) < r00 by A1, A6, 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 A7;
then S . m in Ball (lim S),r0 by METRIC_1:12;
then A8: f . (S . m) in f .: W by A2, A6, FUNCT_1:def 12;
dom T = NAT by FUNCT_2:def 1;
then T . m in f .: W by A1, A8, FUNCT_1:22;
hence dist (T . m),x0 < r by A5, 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