for L being ExtREAL_sequence
for c being ExtReal st ( for n being Nat holds L . n = c ) holds
( L is convergent & lim L = c & lim L = sup (rng L) )