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 A1: ( seq = cseq & seq is convergent & lim seq = rlim ) ; :: thesis: lim cseq = rlim
reconsider clim = rlim as Complex by XCMPLX_0:def 2;
( cseq is convergent & ( 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, Lm1, SEQ_2:def 7;
hence lim cseq = rlim by COMSEQ_2:def 5; :: thesis: verum