let seq be Real_Sequence; :: thesis: for cseq being Complex_Sequence
for rlim being Real st seq = cseq & cseq is convergent & lim cseq = rlim holds
lim seq = rlim
let cseq be Complex_Sequence; :: thesis: for rlim being Real st seq = cseq & cseq is convergent & lim cseq = rlim holds
lim seq = rlim
let rlim be Real; :: thesis: ( seq = cseq & cseq is convergent & lim cseq = rlim implies lim seq = rlim )
assume that
A1: seq = cseq and
A2: cseq is convergent and
A3: lim cseq = rlim ; :: thesis: lim seq = rlim
reconsider clim = rlim as Complex ;
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - rlim).| < p by A1, A2, A3, COMSEQ_2:def 6;
seq is convergent by A1, A2;
hence lim seq = rlim by A4, SEQ_2:def 7; :: thesis: verum