let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is V49() & seq is V89() holds
(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)
let seq be Real_Sequence; :: thesis: ( seq is V49() & seq is V89() implies (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) )
assume A1: ( seq is V49() & seq is V89() ) ; :: thesis: (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)
then (inferior_realsequence seq) . (n + 1) <= seq . n by Th71;
then min (((inferior_realsequence seq) . (n + 1)),(seq . n)) = (inferior_realsequence seq) . (n + 1) by XXREAL_0:def 9;
hence (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) by A1, Th46; :: thesis: verum