theorem :: MESFUNC5:58

for L being ExtREAL_sequence
for K being R_eal st K <> +infty & ( for n being Nat holds L . n <= K ) holds
sup (rng L) < +infty