let n be Nat; :: thesis: for seq being Real_Sequence st seq is non-increasing & seq is bounded_below holds
( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )
let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) )
assume that
A1: seq is non-increasing and
A2: seq is bounded_below ; :: thesis: ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )
reconsider lbs = lower_bound seq as Element of REAL by XREAL_0:def 1;
defpred S₁[ Nat] means (inferior_realsequence seq) . $1 = lbs;
A3: for k being Nat st S₁[k] holds
S₁[k + 1] by A1, A2, Th72;
A4: S₁[ 0 ] by A2, Th38;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A3);
hence ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) by VALUED_0:def 18; :: thesis: verum