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