let X be RealNormSpace; :: thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq

let seq, seq1 be sequence of X; :: thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; :: thesis: lim seq1 = lim seq
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by ;
A4: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p )

assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p

then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
||.((seq . m) - (lim seq)).|| < p by ;
take n = n1; :: thesis: for m being Nat st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((seq1 . m) - (lim seq)).|| < p )
assume A6: n <= m ; :: thesis: ||.((seq1 . m) - (lim seq)).|| < p
A7: m in NAT by ORDINAL1:def 12;
m <= Nseq . m by SEQM_3:14;
then A8: n <= Nseq . m by ;
seq1 . m = seq . (Nseq . m) by ;
hence ||.((seq1 . m) - (lim seq)).|| < p by A5, A8; :: thesis: verum
end;
seq1 is convergent by A1, A2, Th7;
hence lim seq1 = lim seq by ; :: thesis: verum