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 number such that
A2: for n being Element of NAT holds seq . n < t by SEQ_2:def 3;
t is UpperBound of rng seq

proof

let r be ext-real number ; :: 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 set st
( n in dom seq & seq . n = r ) by FUNCT_1:def 5;
hence r <= t by A2; :: thesis: verum

end;

hence rng seq is bounded_above by XXREAL_2:def 10; :: 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 number such that
B3: t is UpperBound of rng seq by XXREAL_2:def 10;
A3: for r being real number st r in rng seq holds
r <= t by B3, XXREAL_2:def 1;

now

let n be Element of NAT ; :: thesis: seq . n < t + 1
seq . n <= t by A3, FUNCT_2:6;
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