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 by XCMPLX_0:def 2;

A4: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p )
assume A5: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p
p is Real by XREAL_0:def 1;
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
|.((cseq . m) - clim).| < p by A2, A3, A5, COMSEQ_2:def 5;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p
thus for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p by A1, A6; :: thesis: verum

end;

seq is convergent by A1, A2, Lm1;
hence lim seq = rlim by A4, SEQ_2:def 7; :: thesis: verum