let seq be Real_Sequence; :: thesis: for cseq being Complex_Sequence

for rlim being Real st seq = cseq & seq is convergent & lim seq = rlim holds

lim cseq = rlim

let cseq be Complex_Sequence; :: thesis: for rlim being Real st seq = cseq & seq is convergent & lim seq = rlim holds

lim cseq = rlim

let rlim be Real; :: thesis: ( seq = cseq & seq is convergent & lim seq = rlim implies lim cseq = rlim )

assume A1: ( seq = cseq & seq is convergent & lim seq = rlim ) ; :: thesis: lim cseq = rlim

reconsider clim = rlim as Element of COMPLEX by XCMPLX_0:def 2;

( cseq is convergent & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((cseq . m) - clim).| < p ) ) by A1, SEQ_2:def 7;

hence lim cseq = rlim by COMSEQ_2:def 6; :: thesis: verum

for rlim being Real st seq = cseq & seq is convergent & lim seq = rlim holds

lim cseq = rlim

let cseq be Complex_Sequence; :: thesis: for rlim being Real st seq = cseq & seq is convergent & lim seq = rlim holds

lim cseq = rlim

let rlim be Real; :: thesis: ( seq = cseq & seq is convergent & lim seq = rlim implies lim cseq = rlim )

assume A1: ( seq = cseq & seq is convergent & lim seq = rlim ) ; :: thesis: lim cseq = rlim

reconsider clim = rlim as Element of COMPLEX by XCMPLX_0:def 2;

( cseq is convergent & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((cseq . m) - clim).| < p ) ) by A1, SEQ_2:def 7;

hence lim cseq = rlim by COMSEQ_2:def 6; :: thesis: verum