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;
A6: now :: thesis: for x being object st x in NAT holds
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;
dom seq = NAT by FUNCT_2:def 1;
hence seq is Real_Sequence by A6, FUNCT_2:3; :: thesis: verum