:: deftheorem Def12 defines lim MESFUNC5:def 12 :
for seq being ExtREAL_sequence st seq is convergent holds
for b₂ being R_eal holds
( b₂ = lim seq iff ( ex g being Real st
( b₂ = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - b₂).| < p ) & seq is convergent_to_finite_number ) or ( b₂ = +infty & seq is convergent_to_+infty ) or ( b₂ = -infty & seq is convergent_to_-infty ) ) );