for seq being Real_Sequence st seq is convergent holds
lim (abs seq) = |.(lim seq).|