let n be Nat; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))
let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) )
reconsider Y2 = { (seq . k) where k is Nat : n + 1 <= k } as Subset of REAL by Th29;
reconsider Y1 = { (seq . k) where k is Nat : n <= k } as Subset of REAL by Th29;
reconsider Y3 = {(seq . n)} as Subset of REAL ;
A1: (superior_realsequence seq) . (n + 1) = upper_bound Y2 by Def5;
assume A2: seq is bounded_above ; :: thesis: (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))
then A3: ( Y2 <> {} & Y2 is bounded_above ) by Th31, SETLIM_1:1;
A4: Y3 is bounded_above

proof

consider t being Real such that
A5: for m being Nat holds seq . m < t by A2, SEQ_2:def 3;
t is UpperBound of Y3

proof

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in Y3 or r <= t )
assume r in Y3 ; :: thesis: r <= t
then r = seq . n by TARSKI:def 1;
hence r <= t by A5; :: thesis: verum

end;

hence Y3 is bounded_above ; :: thesis: verum

end;

(superior_realsequence seq) . n = upper_bound Y1 by Def5;
then (superior_realsequence seq) . n = upper_bound (Y2 \/ Y3) by SETLIM_1:2
.= max ((upper_bound Y2),(upper_bound Y3)) by A3, A4, SEQ_4:143
.= max (((superior_realsequence seq) . (n + 1)),(seq . n)) by A1, SEQ_4:9 ;
hence (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) ; :: thesis: verum