for c being Real
for s, s1 being Real_Sequence st s is convergent & s1 is convergent holds
for r being Real_Sequence st ( for i being Nat holds r . i = (((s . i) - c) * ((s . i) - c)) + (s1 . i) ) holds
( r is convergent & lim r = (((lim s) - c) * ((lim s) - c)) + (lim s1) ) by Lm5;