let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is non-decreasing holds
(inferior_realsequence seq) . n = seq . n
let seq be Real_Sequence; :: thesis: ( seq is non-decreasing implies (inferior_realsequence seq) . n = seq . n )
assume A1: seq is non-decreasing ; :: thesis: (inferior_realsequence seq) . n = seq . n
reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29;
(inferior_realsequence seq) . n = inf Y1 by Def4;
hence (inferior_realsequence seq) . n = seq . n by A1, Th34; :: thesis: verum