for L being ExtREAL_sequence
for n being Nat holds L . n <= sup (rng L)