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 - (seq_const c) is convergent by A1;
then A3: (seq - (seq_const c)) (#) (seq - (seq_const c)) 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_const c)) (#) (seq - (seq_const c))) . i

let i be Element of NAT ; :: thesis: rseq . i = ((seq - (seq_const c)) (#) (seq - (seq_const c))) . i
thus rseq . i = ((seq . i) - c) * ((seq . i) - c) by A4
.= ((seq . i) - ((seq_const c) . i)) * ((seq . i) - c) by SEQ_1:57
.= ((seq . i) - ((seq_const c) . i)) * ((seq . i) + (- ((seq_const c) . i))) by SEQ_1:57
.= ((seq . i) + ((- (seq_const c)) . i)) * ((seq . i) + (- ((seq_const c) . i))) by SEQ_1:10
.= ((seq . i) + ((- (seq_const c)) . i)) * ((seq . i) + ((- (seq_const c)) . i)) by SEQ_1:10
.= ((seq + (- (seq_const c))) . i) * ((seq . i) + ((- (seq_const c)) . i)) by SEQ_1:7
.= ((seq - (seq_const c)) . i) * ((seq + (- (seq_const c))) . i) by SEQ_1:7, SEQ_1:11
.= ((seq - (seq_const c)) . i) * ((seq - (seq_const c)) . i) by SEQ_1:11
.= ((seq - (seq_const c)) (#) (seq - (seq_const c))) . i by SEQ_1:8 ; :: thesis: verum

end;

then A5: for x being object st x in NAT holds
rseq . x = ((seq - (seq_const c)) (#) (seq - (seq_const c))) . x ;
lim ((seq - (seq_const c)) (#) (seq - (seq_const c))) = (lim (seq - (seq_const c))) * (lim (seq - (seq_const c))) by A2, SEQ_2:15
.= ((lim seq) - (lim (seq_const c))) * (lim (seq - (seq_const c))) by A1, SEQ_2:12
.= ((lim seq) - (lim (seq_const c))) * ((lim seq) - (lim (seq_const c))) by A1, SEQ_2:12
.= ((lim seq) - ((seq_const c) . 0)) * ((lim seq) - (lim (seq_const c))) by SEQ_4:26
.= ((lim seq) - ((seq_const c) . 0)) * ((lim seq) - ((seq_const c) . 0)) by SEQ_4:26
.= ((lim seq) - c) * ((lim seq) - ((seq_const c) . 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 A5, A3, FUNCT_2:12; :: thesis: verum