let c be Complex; :: thesis: for seq being Complex_Sequence
for rseq being Real_Sequence st seq is convergent & ( for i being Nat holds rseq . i = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )
let seq be Complex_Sequence; :: thesis: for rseq being Real_Sequence st seq is convergent & ( for i being Nat holds rseq . i = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )
let rseq be Real_Sequence; :: thesis: ( seq is convergent & ( for i being Nat holds rseq . i = |.((seq . i) - c).| ) implies ( rseq is convergent & lim rseq = |.((lim seq) - c).| ) )
assume that
A1: seq is convergent and
A2: for i being Nat holds rseq . i = |.((seq . i) - c).| ; :: thesis: ( rseq is convergent & lim rseq = |.((lim seq) - c).| )
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider cseq = NAT --> c1 as Complex_Sequence ;
A3: for n being Nat holds cseq . n = c by ORDINAL1:def 12, FUNCOP_1:7;
then A4: cseq is convergent by COMSEQ_2:9;
then reconsider seq9 = seq - cseq as convergent Complex_Sequence by A1;
seq - cseq is convergent by A1, A4;
then A5: lim |.(seq - cseq).| = |.(lim (seq - cseq)).| by SEQ_2:27
.= |.((lim seq) - (lim cseq)).| by A1, A4, COMSEQ_2:26
.= |.((lim seq) - c).| by A3, COMSEQ_2:10 ;

now :: thesis: for i being Nat holds rseq . i = |.(seq - cseq).| . i

let i be Nat; :: thesis: rseq . i = |.(seq - cseq).| . i
A6: i in NAT by ORDINAL1:def 12;
thus rseq . i = |.((seq . i) - c).| by A2
.= |.((seq . i) - (cseq . i)).| by FUNCOP_1:7, A6
.= |.((seq . i) + (- (cseq . i))).|
.= |.((seq . i) + ((- cseq) . i)).| by VALUED_1:8
.= |.((seq - cseq) . i).| by VALUED_1:1, A6
.= |.(seq - cseq).| . i by VALUED_1:18 ; :: thesis: verum

end;

then A7: for x being object st x in NAT holds
rseq . x = |.(seq - cseq).| . x ;
|.seq9.| is convergent ;
hence ( rseq is convergent & lim rseq = |.((lim seq) - c).| ) by A7, A5, FUNCT_2:12; :: thesis: verum