for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds
ex k being Nat st seq ^\ k is bounded