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 A2: ex UL being LowerBound of rng seq st UL in REAL by SUPINF_1:def 12;
seq is bounded_above by A1, Def5;
then rng seq is bounded_above by Def4;
then A3: ex UB being UpperBound of rng seq st UB in REAL by SUPINF_1:def 11;

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, XXREAL_0:12, XXREAL_2:def 2;
seq . x <> +infty by 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