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)
A1: sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
dom L = NAT by FUNCT_2:def 1;
then L . n in rng L by FUNCT_1:def 5;
hence L . n <= sup (rng L) by A1, XXREAL_2:def 1; :: thesis: verum