let n be Element of 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) )
assume A1: seq is bounded_above ; :: thesis: (superior_realsequence seq) . n = max ((superior_realsequence seq) . (n + 1)),(seq . n)
reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29;
A2: (superior_realsequence seq) . n = sup Y1 by Def5;
reconsider Y2 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29;
A3: (superior_realsequence seq) . (n + 1) = sup Y2 by Def5;
reconsider Y3 = {(seq . n)} as Subset of REAL ;
A4: ( Y1 <> {} & Y2 <> {} & Y3 <> {} ) by SETLIM_1:1;
A5: ( Y1 is bounded_above & Y2 is bounded_above ) by A1, Th31;
A6: Y3 is bounded_above

proof

consider t being real number such that
A7: for m being Element of NAT holds seq . m < t by A1, SEQ_2:def 3;

now

take t = t; :: thesis: for r being real number st r in Y3 holds
r <= t
let r be real number ; :: thesis: ( r in Y3 implies r <= t )
assume r in Y3 ; :: thesis: r <= t
then r = seq . n by TARSKI:def 1;
hence r <= t by A7; :: thesis: verum

end;

hence Y3 is bounded_above by SEQ_4:def 1; :: thesis: verum

end;

(superior_realsequence seq) . n = sup (Y2 \/ Y3) by A2, SETLIM_1:2
.= max (sup Y2),(sup Y3) by A4, A5, A6, SPRECT_1:53
.= max ((superior_realsequence seq) . (n + 1)),(seq . n) by A3, SEQ_4:22 ;
hence (superior_realsequence seq) . n = max ((superior_realsequence seq) . (n + 1)),(seq . n) ; :: thesis: verum