let c be Real; :: thesis: for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )

reconsider cc = c as Element of REAL by XREAL_0:def 1;
set cseq = seq_const c;
let seq be Real_Sequence; :: thesis: ( seq is convergent implies for rseq being Real_Sequence st ( for i being Nat holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) ) )

assume A1: seq is convergent ; :: thesis: for rseq being Real_Sequence st ( for i being Nat holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )

A2: seq - () is convergent by A1;
then A3: (seq - ()) (#) (seq - ()) is convergent ;
let rseq be Real_Sequence; :: thesis: ( ( for i being Nat holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) implies ( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) ) )
assume A4: 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 Element of NAT holds rseq . i = ((seq - ()) (#) (seq - ())) . i
let i be Element of NAT ; :: thesis: rseq . i = ((seq - ()) (#) (seq - ())) . i
thus rseq . i = ((seq . i) - c) * ((seq . i) - c) by A4
.= ((seq . i) - (() . i)) * ((seq . i) - c) by SEQ_1:57
.= ((seq . i) - (() . i)) * ((seq . i) + (- (() . i))) by SEQ_1:57
.= ((seq . i) + ((- ()) . i)) * ((seq . i) + (- (() . i))) by SEQ_1:10
.= ((seq . i) + ((- ()) . i)) * ((seq . i) + ((- ()) . i)) by SEQ_1:10
.= ((seq + (- ())) . i) * ((seq . i) + ((- ()) . i)) by SEQ_1:7
.= ((seq - ()) . i) * ((seq + (- ())) . i) by
.= ((seq - ()) . i) * ((seq - ()) . i) by SEQ_1:11
.= ((seq - ()) (#) (seq - ())) . i by SEQ_1:8 ; :: thesis: verum
end;
then A5: for x being object st x in NAT holds
rseq . x = ((seq - ()) (#) (seq - ())) . x ;
lim ((seq - ()) (#) (seq - ())) = (lim (seq - ())) * (lim (seq - ())) by
.= ((lim seq) - (lim ())) * (lim (seq - ())) by
.= ((lim seq) - (lim ())) * ((lim seq) - (lim ())) by
.= ((lim seq) - (() . 0)) * ((lim seq) - (lim ())) by SEQ_4:26
.= ((lim seq) - (() . 0)) * ((lim seq) - (() . 0)) by SEQ_4:26
.= ((lim seq) - c) * ((lim seq) - (() . 0)) by SEQ_1:57
.= ((lim seq) - c) * ((lim seq) - c) by SEQ_1:57 ;
hence ( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) ) by ; :: thesis: verum