let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_above iff rseq is bounded_above )
let rseq be Real_Sequence; :: thesis: ( seq = rseq implies ( seq is bounded_above iff rseq is bounded_above ) )
assume A1: seq = rseq ; :: thesis: ( seq is bounded_above iff rseq is bounded_above )

hereby :: thesis: ( rseq is bounded_above implies seq is bounded_above )

assume seq is bounded_above ; :: thesis: rseq is bounded_above
then rng rseq is bounded_above by A1;
then consider p being Real such that
A2: p is UpperBound of rng rseq by XXREAL_2:def 10;
A3: for y being Real st y in rng rseq holds
y <= p by A2, XXREAL_2:def 1;

now :: thesis: for n being Nat holds rseq . n < p + 1

let n be Nat; :: thesis: rseq . n < p + 1
n in NAT by ORDINAL1:def 12;
then rseq . n in rng rseq by FUNCT_2:4;
then 0 + (rseq . n) < 1 + p by A3, XREAL_1:8;
hence rseq . n < p + 1 ; :: thesis: verum

end;

hence rseq is bounded_above by SEQ_2:def 3; :: thesis: verum

end;

assume rseq is bounded_above ; :: thesis: seq is bounded_above
then consider q being Real such that
A4: for n being Nat holds rseq . n < q by SEQ_2:def 3;

now :: thesis: for r being ExtReal st r in rng seq holds
r <= q

let r be ExtReal; :: thesis: ( r in rng seq implies r <= q )
assume r in rng seq ; :: thesis: r <= q
then ex x being object st
( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def 3;
hence r <= q by A4; :: thesis: verum

end;

then q is UpperBound of rng seq by XXREAL_2:def 1;
hence rng seq is bounded_above by XXREAL_2:def 10; :: according to RINFSUP2:def 4 :: thesis: verum