let seq be ExtREAL_sequence; :: thesis:
let rseq be Real_Sequence; :: thesis:
assume that
A1: seq = rseq and
A2: rseq is bounded ; :: thesis:
A3: NAT = dom (superior_realsequence rseq) by FUNCT_2:def 1;

A4: now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;

let x be object ; :: thesis:
assume x in { (rseq . k) where k is Nat : n <= k } ; :: thesis:
then ex k being Nat st
( x = rseq . k & n <= k ) ;
hence x in REAL by XREAL_0:def 1; :: thesis:

end;

then reconsider Y2 = { (rseq . k) where k is Nat : n <= k } as Subset of REAL by TARSKI:def 3;
A5: Y2 is bounded_above by A2, RINFSUP1:31;
ex Y1 being non empty Subset of ExtREAL st
( Y1 = { (seq . k) where k is Nat : n <= k } & (superior_realsequence seq) . n = sup Y1 ) by Def7;
then (superior_realsequence seq) . x = upper_bound Y2 by A1, A5, Th1;
hence (superior_realsequence seq) . x = (superior_realsequence rseq) . x by RINFSUP1:def 5; :: thesis:

end;

superior_realsequence rseq is bounded by A2, RINFSUP1:56;
then A6: rng (superior_realsequence rseq) is bounded_below by RINFSUP1:6;
NAT = dom (superior_realsequence seq) by FUNCT_2:def 1;
then superior_realsequence seq = superior_realsequence rseq by A4, A3, FUNCT_1:2;
hence ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) by A6, Th3; :: thesis: