:: deftheorem defines convergent_to_finite_number MESFUNC5:def 8 :
for seq being ExtREAL_sequence holds
( seq is convergent_to_finite_number iff ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p );