let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq & rseq is bounded holds

( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )

let rseq be Real_Sequence; :: thesis: ( seq = rseq & rseq is bounded implies ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) )

assume that

A1: seq = rseq and

A2: rseq is bounded ; :: thesis: ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )

A3: NAT = dom (inferior_realsequence rseq) by FUNCT_2:def 1;

then A7: rng (inferior_realsequence rseq) is bounded_above by RINFSUP1:5;

NAT = dom (inferior_realsequence seq) by FUNCT_2:def 1;

then inferior_realsequence seq = inferior_realsequence rseq by A4, A3, FUNCT_1:2;

hence ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) by A7, Th1; :: thesis: verum

( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )

let rseq be Real_Sequence; :: thesis: ( seq = rseq & rseq is bounded implies ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) )

assume that

A1: seq = rseq and

A2: rseq is bounded ; :: thesis: ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )

A3: NAT = dom (inferior_realsequence rseq) by FUNCT_2:def 1;

A4: now :: thesis: for x being object st x in NAT holds

(inferior_realsequence seq) . x = (inferior_realsequence rseq) . x

inferior_realsequence rseq is bounded
by A2, RINFSUP1:56;(inferior_realsequence seq) . x = (inferior_realsequence rseq) . x

let x be object ; :: thesis: ( x in NAT implies (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x )

assume x in NAT ; :: thesis: (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x

then reconsider n = x as Element of NAT ;

consider Y1 being non empty Subset of ExtREAL such that

A5: Y1 = { (seq . k) where k is Nat : n <= k } and

A6: (inferior_realsequence seq) . n = inf Y1 by Def6;

Y2 is bounded_below by A2, RINFSUP1:32;

then inf Y1 = lower_bound Y2 by A1, A5, Th3;

hence (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x by A6, RINFSUP1:def 4; :: thesis: verum

end;assume x in NAT ; :: thesis: (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x

then reconsider n = x as Element of NAT ;

consider Y1 being non empty Subset of ExtREAL such that

A5: Y1 = { (seq . k) where k is Nat : n <= k } and

A6: (inferior_realsequence seq) . n = inf Y1 by Def6;

now :: thesis: for x being object st x in { (rseq . k) where k is Nat : n <= k } holds

x in REAL

then reconsider Y2 = { (rseq . k) where k is Nat : n <= k } as Subset of REAL by TARSKI:def 3;x in REAL

let x be object ; :: thesis: ( x in { (rseq . k) where k is Nat : n <= k } implies x in REAL )

assume x in { (rseq . k) where k is Nat : n <= k } ; :: thesis: x in REAL

then ex k being Nat st

( x = rseq . k & n <= k ) ;

hence x in REAL by XREAL_0:def 1; :: thesis: verum

end;assume x in { (rseq . k) where k is Nat : n <= k } ; :: thesis: x in REAL

then ex k being Nat st

( x = rseq . k & n <= k ) ;

hence x in REAL by XREAL_0:def 1; :: thesis: verum

Y2 is bounded_below by A2, RINFSUP1:32;

then inf Y1 = lower_bound Y2 by A1, A5, Th3;

hence (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x by A6, RINFSUP1:def 4; :: thesis: verum

then A7: rng (inferior_realsequence rseq) is bounded_above by RINFSUP1:5;

NAT = dom (inferior_realsequence seq) by FUNCT_2:def 1;

then inferior_realsequence seq = inferior_realsequence rseq by A4, A3, FUNCT_1:2;

hence ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) by A7, Th1; :: thesis: verum