for seq being Real_Sequence st seq is convergent holds
abs seq is convergent