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