let n be Nat; :: thesis: for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)
let seq be Real_Sequence; :: thesis: (superior_realsequence seq) . n = upper_bound (seq ^\ n)
reconsider Y = { (seq . k) where k is Nat : n <= k } as Subset of REAL by Th29;
(superior_realsequence seq) . n = upper_bound Y by Def5
.= upper_bound (rng (seq ^\ n)) by Th30 ;
hence (superior_realsequence seq) . n = upper_bound (seq ^\ n) ; :: thesis: verum