let n be Nat; for seq being Real_Sequence st seq is V96() holds
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
let seq be Real_Sequence; ( seq is V96() implies (inferior_realsequence seq) . n = min (((inferior_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:
(inferior_realsequence seq) . (n + 1) = lower_bound Y2
by Def4;
assume A2:
seq is V96()
; (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
then A3:
( Y2 <> {} & Y2 is bounded_below )
by Th32, SETLIM_1:1;
A4:
Y3 is bounded_below
(inferior_realsequence seq) . n = lower_bound Y1
by Def4;
then (inferior_realsequence seq) . n =
lower_bound (Y2 \/ Y3)
by SETLIM_1:2
.=
min ((lower_bound Y2),(lower_bound Y3))
by A3, A4, SEQ_4:142
.=
min (((inferior_realsequence seq) . (n + 1)),(seq . n))
by A1, SEQ_4:9
;
hence
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
; verum