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

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