let seq be Real_Sequence; :: thesis: ( seq is bounded_above iff rng seq is bounded_above )
A1: ( seq is bounded_above implies rng seq is bounded_above )

proof

assume seq is bounded_above ; :: thesis: rng seq is bounded_above
then consider t being Real such that
A2: for n being Nat holds seq . n < t by SEQ_2:def 3;
t is UpperBound of rng seq

proof

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in rng seq or r <= t )
assume r in rng seq ; :: thesis: r <= t
then ex n being object st
( n in dom seq & seq . n = r ) by FUNCT_1:def 3;
hence r <= t by A2; :: thesis: verum

end;

hence rng seq is bounded_above ; :: thesis: verum

end;

( rng seq is bounded_above implies seq is bounded_above )

proof

assume rng seq is bounded_above ; :: thesis: seq is bounded_above
then consider t being Real such that
A3: t is UpperBound of rng seq ;
A4: for r being Real st r in rng seq holds
r <= t by A3, XXREAL_2:def 1;

now :: thesis: for n being Nat holds seq . n < t + 1

let n be Nat; :: thesis: seq . n < t + 1
A5: n in NAT by ORDINAL1:def 12;
seq . n <= t by A4, FUNCT_2:4, A5;
hence seq . n < t + 1 by Lm1; :: thesis: verum

end;

hence seq is bounded_above by SEQ_2:def 3; :: thesis: verum

end;

hence ( seq is bounded_above iff rng seq is bounded_above ) by A1; :: thesis: verum