let L be ExtREAL_sequence; :: thesis: for n being Nat holds L . n <= sup (rng L)
let n be Nat; :: thesis: L . n <= sup (rng L)
reconsider n = n as Element of NAT by ORDINAL1:def 12;
dom L = NAT by FUNCT_2:def 1;
then A1: L . n in rng L by FUNCT_1:def 3;
sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;
hence L . n <= sup (rng L) by A1, XXREAL_2:def 1; :: thesis: verum