let X be non empty MetrSpace; :: thesis: for x being Element of X
for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds
S1 is_convergent_in_metrspace_to x
let x be Element of X; :: thesis: for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds
S1 is_convergent_in_metrspace_to x
let S, S1 be sequence of X; :: thesis: ( S is_convergent_in_metrspace_to x & S1 is subsequence of S implies S1 is_convergent_in_metrspace_to x )
assume that
A1: S is_convergent_in_metrspace_to x and
A2: S1 is subsequence of S ; :: thesis: S1 is_convergent_in_metrspace_to x
consider Nseq being increasing sequence of NAT such that
A3: S1 = S * Nseq by A2, VALUED_0:def 17;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
dist ((S1 . n),x) < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
dist ((S1 . n),x) < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
dist ((S1 . n),x) < r
then consider m1 being Nat such that
A4: for n being Nat st m1 <= n holds
dist ((S . n),x) < r by A1;
take m = m1; :: thesis: for n being Nat st m <= n holds
dist ((S1 . n),x) < r
for n being Nat st m <= n holds
dist ((S1 . n),x) < r

proof

let n be Nat; :: thesis: ( m <= n implies dist ((S1 . n),x) < r )
assume A5: m <= n ; :: thesis: dist ((S1 . n),x) < r
A6: n in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then ( dom Nseq = NAT & Nseq . n in dom S ) by FUNCT_2:def 1;
then n in dom (S * Nseq) by FUNCT_1:11, A6;
then A7: S1 . n = S . (Nseq . n) by A3, FUNCT_1:12;
n <= Nseq . n by SEQM_3:14;
then m1 <= Nseq . n by A5, XXREAL_0:2;
hence dist ((S1 . n),x) < r by A4, A7; :: thesis: verum

end;

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

end;

hence S1 is_convergent_in_metrspace_to x ; :: thesis: verum