let c be Complex; :: thesis: for seq being Complex_Sequence
for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
let seq be Complex_Sequence; :: thesis: for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
let seq1 be Real_Sequence; :: thesis: ( seq is convergent & seq1 is convergent implies for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) )
assume that
A1: seq is convergent and
A2: seq1 is convergent ; :: thesis: for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
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: lim cseq = c by COMSEQ_2:10
.= cseq . 0 by FUNCOP_1:7 ;
A5: cseq is convergent by A3, COMSEQ_2:9;
then seq - cseq is convergent by A1;
then A6: lim |.(seq - cseq).| = |.(lim (seq - cseq)).| by SEQ_2:27
.= |.((lim seq) - (cseq . 0)).| by A1, A4, A5, COMSEQ_2:26
.= |.((lim seq) - c).| by FUNCOP_1:7 ;
let rseq be Real_Sequence; :: thesis: ( ( for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) implies ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) )
assume A7: for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ; :: thesis: ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )

now :: thesis: for i being Element of NAT holds rseq . i = (|.(seq - cseq).| + seq1) . i

let i be Element of NAT ; :: thesis: rseq . i = (|.(seq - cseq).| + seq1) . i
thus rseq . i = |.((seq . i) - c).| + (seq1 . i) by A7
.= |.((seq . i) - (cseq . i)).| + (seq1 . i) by FUNCOP_1:7
.= |.((seq . i) + (- (cseq . i))).| + (seq1 . i)
.= |.((seq . i) + ((- cseq) . i)).| + (seq1 . i) by VALUED_1:8
.= |.((seq - cseq) . i).| + (seq1 . i) by VALUED_1:1
.= (|.(seq - cseq).| . i) + (seq1 . i) by VALUED_1:18
.= (|.(seq - cseq).| + seq1) . i by SEQ_1:7 ; :: thesis: verum

end;

then A8: rseq = |.(seq - cseq).| + seq1 by FUNCT_2:63;
reconsider seq1 = seq - cseq as convergent Complex_Sequence by A1, A5;
|.seq1.| is convergent ;
hence ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) by A2, A8, A6, SEQ_2:6; :: thesis: verum