let seq be ExtREAL_sequence; :: thesis: ( seq is bounded implies seq is Real_Sequence )
assume A1: seq is bounded ; :: thesis: seq is Real_Sequence
then seq is bounded_above by Def5;
then rng seq is bounded_above by Def4;
then consider UB being UpperBound of rng seq such that
A2: UB in REAL by SUPINF_1:def 11;
seq is bounded_below by A1, Def5;
then rng seq is bounded_below by Def3;
then consider UL being LowerBound of rng seq such that
A3: UL in REAL by SUPINF_1:def 12;
A4: dom seq = NAT by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in NAT implies seq . x in REAL )
assume x in NAT ; :: thesis: seq . x in REAL
then A5: seq . x in rng seq by FUNCT_2:6;
( UB < +infty & -infty < UL ) by A2, A3, XXREAL_0:9, XXREAL_0:12;
then ( seq . x <> +infty & seq . x <> -infty ) by A5, XXREAL_2:def 1, XXREAL_2:def 2;
then seq . x is Real by XXREAL_0:14;
hence seq . x in REAL ; :: thesis: verum

end;

hence seq is Real_Sequence by A4, FUNCT_2:5; :: thesis: verum