let c be Real; :: thesis: for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )
reconsider cseq = NAT --> c as Real_Sequence ;
let seq be Real_Sequence; :: thesis: ( seq is convergent implies for rseq being Real_Sequence st ( for i being Element of 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 Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )
A2: seq - cseq is convergent by A1, SEQ_2:25;
then A3: (seq - cseq) (#) (seq - cseq) is convergent by SEQ_2:28;
let rseq be Real_Sequence; :: thesis: ( ( for i being Element of 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 Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ; :: thesis: ( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )

now

let i be Element of NAT ; :: thesis: rseq . i = ((seq - cseq) (#) (seq - cseq)) . i
thus rseq . i = ((seq . i) - c) * ((seq . i) - c) by A4
.= ((seq . i) - (cseq . i)) * ((seq . i) - c) by FUNCOP_1:13
.= ((seq . i) - (cseq . i)) * ((seq . i) + (- (cseq . i))) by FUNCOP_1:13
.= ((seq . i) + ((- cseq) . i)) * ((seq . i) + (- (cseq . i))) by SEQ_1:14
.= ((seq . i) + ((- cseq) . i)) * ((seq . i) + ((- cseq) . i)) by SEQ_1:14
.= ((seq + (- cseq)) . i) * ((seq . i) + ((- cseq) . i)) by SEQ_1:11
.= ((seq + (- cseq)) . i) * ((seq + (- cseq)) . i) by SEQ_1:11
.= ((seq - cseq) . i) * ((seq + (- cseq)) . i) by SEQ_1:15
.= ((seq - cseq) . i) * ((seq - cseq) . i) by SEQ_1:15
.= ((seq - cseq) (#) (seq - cseq)) . i by SEQ_1:12 ; :: thesis: verum

end;

then A5: for x being set st x in NAT holds
rseq . x = ((seq - cseq) (#) (seq - cseq)) . x ;
lim ((seq - cseq) (#) (seq - cseq)) = (lim (seq - cseq)) * (lim (seq - cseq)) by A2, SEQ_2:29
.= ((lim seq) - (lim cseq)) * (lim (seq - cseq)) by A1, SEQ_2:26
.= ((lim seq) - (lim cseq)) * ((lim seq) - (lim cseq)) by A1, SEQ_2:26
.= ((lim seq) - (cseq . 0 )) * ((lim seq) - (lim cseq)) by SEQ_4:41
.= ((lim seq) - (cseq . 0 )) * ((lim seq) - (cseq . 0 )) by SEQ_4:41
.= ((lim seq) - c) * ((lim seq) - (cseq . 0 )) by FUNCOP_1:13
.= ((lim seq) - c) * ((lim seq) - c) by FUNCOP_1:13 ;
hence ( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) ) by A5, A3, FUNCT_2:18; :: thesis: verum