let rseq be Real_Sequence; :: thesis: ( rseq is bounded implies for n being Element of NAT holds rseq . n <= sup (rng rseq) )
assume rseq is bounded ; :: thesis: for n being Element of NAT holds rseq . n <= sup (rng rseq)
then rng rseq is bounded by PSCOMP_1:7;
then A1: rng rseq is bounded_above by XXREAL_2:def 11;
let n be Element of NAT ; :: thesis: rseq . n <= sup (rng rseq)
NAT = dom rseq by FUNCT_2:def 1;
then rseq . n in rng rseq by FUNCT_1:12;
hence rseq . n <= sup (rng rseq) by A1, SEQ_4:def 4; :: thesis: verum