let n be Nat; :: thesis: for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )
let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) )
reconsider ubs = upper_bound seq as Element of REAL by XREAL_0:def 1;
defpred S₁[ Nat] means (superior_realsequence seq) . $1 = ubs;
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )
A2: for k being Nat st S₁[k] holds
S₁[k + 1] by A1, Th66;
A3: S₁[ 0 ] by A1, Th39;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A2);
hence ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) by VALUED_0:def 18; :: thesis: verum