let seq be Real_Sequence; :: thesis: for cseq being Complex_Sequence
for rlim being real number st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim
let cseq be Complex_Sequence; :: thesis: for rlim being real number st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim
let rlim be real number ; :: thesis: ( seq = cseq & seq is convergent & lim seq = rlim implies lim cseq = rlim )
assume that
A1: seq = cseq and
A2: seq is convergent and
A4: lim seq = rlim ; :: thesis: lim cseq = rlim
reconsider clim = rlim as Complex by XCMPLX_0:def 2;
A5: cseq is convergent by A1, A2, LM03;
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
abs ((cseq . m) - clim) < p by A1, A2, A4, SEQ_2:def 7;
hence lim cseq = rlim by A5, COMSEQ_2:def 5; :: thesis: verum