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_below by Def5;
then rng seq is bounded_below by Def3;
then consider UL being real number such that
A2: UL is LowerBound of rng seq by XXREAL_2:def 9;
A3: UL in REAL by XREAL_0:def 1;
seq is bounded_above by A1, Def5;
then rng seq is bounded_above by Def4;
then consider UB being real number such that
A4: UB is UpperBound of rng seq by XXREAL_2:def 10;
A5: UB in REAL by XREAL_0:def 1;

A6: now

let x be set ; :: thesis: ( x in NAT implies seq . x in REAL )
assume x in NAT ; :: thesis: seq . x in REAL
then A7: seq . x in rng seq by FUNCT_2:4;
then A8: seq . x <> -infty by A2, A3, XXREAL_0:12, XXREAL_2:def 2;
seq . x <> +infty by A5, A4, A7, XXREAL_0:9, XXREAL_2:def 1;
hence seq . x in REAL by A8, XXREAL_0:14; :: thesis: verum

end;

dom seq = NAT by FUNCT_2:def 1;
hence seq is Real_Sequence by A6, FUNCT_2:3; :: thesis: verum