let rseq be Real_Sequence; :: thesis: for K being Real st ( for n being Nat holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
let K be Real; :: thesis: ( ( for n being Nat holds rseq . n <= K ) implies upper_bound (rng rseq) <= K )
assume A1: for n being Nat holds rseq . n <= K ; :: thesis: upper_bound (rng rseq) <= K

now :: thesis: for s being Real st s in rng rseq holds
s <= K

let s be Real; :: thesis: ( s in rng rseq implies s <= K )
assume s in rng rseq ; :: thesis: s <= K
then ex n being object st
( n in NAT & rseq . n = s ) by FUNCT_2:11;
hence s <= K by A1; :: thesis: verum

end;

hence upper_bound (rng rseq) <= K by SEQ_4:45; :: thesis: verum