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

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

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

end;

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