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 ;

then rng seq is bounded_below ;

then consider UL being Real 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;

then rng seq is bounded_above ;

then consider UB being Real such that

A4: UB is UpperBound of rng seq by XXREAL_2:def 10;

A5: UB in REAL by XREAL_0:def 1;

hence seq is Real_Sequence by A6, FUNCT_2:3; :: thesis: verum

assume A1: seq is bounded ; :: thesis: seq is Real_Sequence

then seq is bounded_below ;

then rng seq is bounded_below ;

then consider UL being Real 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;

then rng seq is bounded_above ;

then consider UB being Real 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 :: thesis: for x being object st x in NAT holds

seq . x in REAL

dom seq = NAT
by FUNCT_2:def 1;seq . x in REAL

let x be object ; :: 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;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

hence seq is Real_Sequence by A6, FUNCT_2:3; :: thesis: verum