theorem :: SEQ_2:9

for seq being Real_Sequence st seq is convergent holds
- seq is convergent ;