theorem Th47: :: RINFSUP1:47

for n being Nat
for seq being Real_Sequence st seq is bounded_above holds
(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))