for seq being Real_Sequence st seq is convergent holds
lim (- seq) = - (lim seq)