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

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