let seq1, seq be Complex_Sequence; :: 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 g being Element of COMPLEX such that
A3: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p by A2, COMSEQ_2:def 4;
take t = g; :: according to COMSEQ_2:def 4 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.((seq1 . b₃) - t).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.((seq1 . b₂) - t).| ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.((seq1 . b₂) - t).| )
then consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g).| < p by A3;
take n = n1; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= |.((seq1 . b₁) - t).| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= |.((seq1 . m) - t).| )
assume A5: n <= m ; :: thesis: not p <= |.((seq1 . m) - t).|
consider Nseq being V36() sequence of NAT such that
A6: seq1 = seq * Nseq by A1, VALUED_0:def 17;
m <= Nseq . m by SEQM_3:33;
then A7: n <= Nseq . m by A5, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A6, FUNCT_2:21;
hence |.((seq1 . m) - t).| < p by A4, A7; :: thesis: verum