let X be ComplexNormSpace; :: 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 :: 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 A2, CLVECT_1:def 16;
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 A6, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15, A7;
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 A4, CLVECT_1:def 16; :: thesis: verum