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