for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds
( rseq is convergent & lim seq = lim rseq )