let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_above )
assume A1: seq is bounded_above ; :: thesis: for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_above
let n be Nat; :: thesis: for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_above
set seq1 = seq ^\ n;
seq ^\ n is bounded_above by A1, SEQM_3:27;
then A2: rng (seq ^\ n) is bounded_above by Th5;
let R be Subset of REAL; :: thesis: ( R = { (seq . k) where k is Nat : n <= k } implies R is bounded_above )
assume R = { (seq . k) where k is Nat : n <= k } ; :: thesis: R is bounded_above
hence R is bounded_above by A2, Th30; :: thesis: verum