:: deftheorem defines convergent MESFUNC5:def 11 :
for seq being ExtREAL_sequence holds
( seq is convergent iff ( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty ) );