let X, Y be non empty MetrSpace; :: thesis: for f being Function of (),()
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 (),(); :: 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 () by TOPMETR:12;
A4: dom f = the carrier of () by FUNCT_2:def 1
.= the carrier of X by TOPMETR:12 ;
then f . (lim S) in rng f by FUNCT_1:def 3;
then reconsider x0 = f . (lim S) as Element of Y by TOPMETR:12;
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 () by TOPMETR:12;
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 ;
then consider W being Subset of () such that
A5: ( p in W & W is open ) and
A6: f .: W c= V by ;
consider r0 being Real such that
A7: r0 > 0 and
A8: Ball ((lim S),r0) c= W by ;
reconsider r00 = r0 as Real ;
consider n0 being Nat such that
A9: for m being Nat st n0 <= m holds
dist ((S . m),(lim S)) < r00 by ;
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 A9;
then S . m in Ball ((lim S),r0) by METRIC_1:11;
then A10: f . (S . m) in f .: W by ;
A11: m in NAT by ORDINAL1:def 12;
dom T = NAT by FUNCT_2:def 1;
then T . m in f .: W by ;
hence dist ((T . m),x0) < r by ; :: 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 by TBSP_1:def 2; :: thesis: verum