let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq & rseq is bounded holds
( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq )
let rseq be Real_Sequence; :: thesis: ( seq = rseq & rseq is bounded implies ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) )
assume A1: ( seq = rseq & rseq is bounded ) ; :: thesis: ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq )

A2: now

let x be set ; :: thesis: ( x in NAT implies (superior_realsequence seq) . x = (superior_realsequence rseq) . x )
assume x in NAT ; :: thesis: (superior_realsequence seq) . x = (superior_realsequence rseq) . x
then reconsider n = x as Element of NAT ;
A3: ex Y1 being non empty Subset of ExtREAL st
( Y1 = { (seq . k) where k is Element of NAT : n <= k } & (superior_realsequence seq) . n = sup Y1 ) by Def7;
{ (rseq . k) where k is Element of NAT : n <= k } is Subset of REAL

proof

now

let x be set ; :: thesis: ( x in { (rseq . k) where k is Element of NAT : n <= k } implies x in REAL )
assume x in { (rseq . k) where k is Element of NAT : n <= k } ; :: thesis: x in REAL
then ex k being Element of NAT st
( x = rseq . k & n <= k ) ;
hence x in REAL ; :: thesis: verum

end;

hence { (rseq . k) where k is Element of NAT : n <= k } is Subset of REAL by TARSKI:def 3; :: thesis: verum

end;

then reconsider Y2 = { (rseq . k) where k is Element of NAT : n <= k } as Subset of REAL ;
rseq is bounded_above by A1;
then Y2 is bounded_above by RINFSUP1:31;
then (superior_realsequence seq) . x = upper_bound Y2 by A1, A3, Th1;
hence (superior_realsequence seq) . x = (superior_realsequence rseq) . x by RINFSUP1:def 5; :: thesis: verum

end;

( NAT = dom (superior_realsequence seq) & NAT = dom (superior_realsequence rseq) ) by FUNCT_2:def 1;
then A4: superior_realsequence seq = superior_realsequence rseq by A2, FUNCT_1:9;
superior_realsequence rseq is bounded by A1, RINFSUP1:58;
then superior_realsequence rseq is bounded_below ;
then rng (superior_realsequence rseq) is bounded_below by RINFSUP1:6;
hence ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) by A4, Th3; :: thesis: verum