let c be Complex; :: thesis: for seq1 being Real_Sequence
for seq being Complex_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).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )

let seq1 be Real_Sequence; :: thesis: for seq being Complex_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).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )

let seq be Complex_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).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((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).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((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 ;
then A4: cseq is convergent by COMSEQ_2:9;
then reconsider s = seq - cseq as convergent Complex_Sequence by A1;
A5: |.s.| is convergent ;
then A6: |.(seq - cseq).| (#) |.(seq - cseq).| is convergent ;
let rseq be Real_Sequence; :: thesis: ( ( for i being Nat holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) implies ( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) )
assume A7: for i being Nat holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ; :: thesis: ( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
now :: thesis: for i being Element of NAT holds rseq . i = ((|.(seq - cseq).| (#) |.(seq - cseq).|) + seq1) . i
let i be Element of NAT ; :: thesis: rseq . i = ((|.(seq - cseq).| (#) |.(seq - cseq).|) + seq1) . i
thus rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) by A7
.= (|.((seq . i) - (cseq . i)).| * |.((seq . i) - c).|) + (seq1 . i) by FUNCOP_1:7
.= (|.((seq . i) - (cseq . i)).| * |.((seq . i) - (cseq . i)).|) + (seq1 . i) by FUNCOP_1:7
.= (|.((seq . i) + ((- cseq) . i)).| * |.((seq . i) + (- (cseq . i))).|) + (seq1 . i) by VALUED_1:8
.= (|.((seq . i) + ((- cseq) . i)).| * |.((seq . i) + ((- cseq) . i)).|) + (seq1 . i) by VALUED_1:8
.= (|.((seq + (- cseq)) . i).| * |.((seq . i) + ((- cseq) . i)).|) + (seq1 . i) by VALUED_1:1
.= (|.((seq - cseq) . i).| * |.((seq + (- cseq)) . i).|) + (seq1 . i) by VALUED_1:1
.= ((|.(seq - cseq).| . i) * |.((seq - cseq) . i).|) + (seq1 . i) by VALUED_1:18
.= ((|.(seq - cseq).| . i) * (|.(seq - cseq).| . i)) + (seq1 . i) by VALUED_1:18
.= ((|.(seq - cseq).| (#) |.(seq - cseq).|) . i) + (seq1 . i) by SEQ_1:8
.= ((|.(seq - cseq).| (#) |.(seq - cseq).|) + seq1) . i by SEQ_1:7 ; :: thesis: verum
end;
then A8: rseq = (|.(seq - cseq).| (#) |.(seq - cseq).|) + seq1 by FUNCT_2:63;
lim (|.(seq - cseq).| (#) |.(seq - cseq).|) = (lim |.(seq - cseq).|) * (lim |.(seq - cseq).|) by
.= |.((lim seq) - (lim cseq)).| * (lim |.(seq - cseq).|) by
.= |.((lim seq) - (lim cseq)).| * |.((lim seq) - (lim cseq)).| by
.= |.((lim seq) - c).| * |.((lim seq) - (lim cseq)).| by
.= |.((lim seq) - c).| * |.((lim seq) - c).| by ;
hence ( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by ; :: thesis: verum