let X be ComplexNormSpace; :: thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
let seq, seq1 be sequence of X; :: thesis: ( seq1 is subsequence of seq & seq is convergent implies seq1 is convergent )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; :: thesis: seq1 is convergent
consider g1 being Element of X such that
A3: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - g1).|| < p by A2;
take g1 ; :: according to CLVECT_1:def 15 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= ||.((seq1 . b₃) - g1).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.((seq1 . b₂) - g1).|| ) )
assume 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.((seq1 . b₂) - g1).|| )
then consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
||.((seq . m) - g1).|| < p by A3;
take n = n1; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= ||.((seq1 . b₁) - g1).|| )
let m be Nat; :: thesis: ( not n <= m or not p <= ||.((seq1 . m) - g1).|| )
assume A5: n <= m ; :: thesis: not p <= ||.((seq1 . m) - g1).||
A6: m in NAT by ORDINAL1:def 12;
consider Nseq being increasing sequence of NAT such that
A7: seq1 = seq * Nseq by A1, VALUED_0:def 17;
m <= Nseq . m by SEQM_3:14;
then A8: n <= Nseq . m by A5, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A7, FUNCT_2:15, A6;
hence not p <= ||.((seq1 . m) - g1).|| by A4, A8; :: thesis: verum