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