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:12;

A4: dom f = the carrier of (TopSpaceMetr X) 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

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:12;

A4: dom f = the carrier of (TopSpaceMetr X) 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

hence
T is convergent
by TBSP_1:def 2; :: thesis: verum
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) 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 GOBOARD6:1, TOPMETR:14;

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:10;

consider r0 being Real such that

A7: r0 > 0 and

A8: Ball ((lim S),r0) c= W by A5, TOPMETR:15;

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 A1, A7, TBSP_1:def 3;

for m being Nat st n0 <= m holds

dist ((T . m),x0) < r

for m being Nat st n <= m holds

dist ((T . m),x0) < r ; :: thesis: verum

end;for m being Nat st n <= m holds

dist ((T . m),x0) < r )

reconsider V = Ball (x0,r) as Subset of (TopSpaceMetr Y) 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 GOBOARD6:1, TOPMETR:14;

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:10;

consider r0 being Real such that

A7: r0 > 0 and

A8: Ball ((lim S),r0) c= W by A5, TOPMETR:15;

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 A1, A7, TBSP_1:def 3;

for m being Nat st n0 <= m holds

dist ((T . m),x0) < r

proof

hence
ex n being Nat st
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 A4, A8, FUNCT_1:def 6;

A11: m in NAT by ORDINAL1:def 12;

dom T = NAT by FUNCT_2:def 1;

then T . m in f .: W by A2, A10, FUNCT_1:12, A11;

hence dist ((T . m),x0) < r by A6, METRIC_1:11; :: thesis: verum

end;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 A4, A8, FUNCT_1:def 6;

A11: m in NAT by ORDINAL1:def 12;

dom T = NAT by FUNCT_2:def 1;

then T . m in f .: W by A2, A10, FUNCT_1:12, A11;

hence dist ((T . m),x0) < r by A6, METRIC_1:11; :: thesis: verum

for m being Nat st n <= m holds

dist ((T . m),x0) < r ; :: thesis: verum