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 A1, VALUED_0:def 17;

A4: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
||.((seq . m) - (lim seq)).|| < p by A2, NORMSP_1:def 7;
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.((seq1 . m) - (lim seq)).|| < p )
assume A6: n <= m ; :: thesis: ||.((seq1 . m) - (lim seq)).|| < p
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A6, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15;
hence ||.((seq1 . m) - (lim seq)).|| < p by A5, A7; :: thesis: verum

end;

seq1 is convergent by A1, A2, Th11;
hence lim seq1 = lim seq by A4, NORMSP_1:def 7; :: thesis: verum