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;
B2: 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
A3: UB is UpperBound of rng seq by XXREAL_2:def 10;
B3: UB in REAL by XREAL_0:def 1;

A4: 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;
then A6: seq . x <> -infty by A2, B2, XXREAL_0:12, XXREAL_2:def 2;
seq . x <> +infty by B3, A3, A5, XXREAL_0:9, XXREAL_2:def 1;
hence seq . x in REAL by A6, XXREAL_0:14; :: thesis: verum

end;

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