let seq be Real_Sequence; :: thesis: ( seq is bounded iff ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) )
thus ( seq is bounded implies ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) ) :: thesis: ( ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) implies seq is bounded )

proof

assume A1: seq is bounded ; :: thesis: ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) )
then consider r1 being real number such that
A2: for n being Element of NAT holds seq . n < r1 by Def3;
consider r2 being real number such that
A3: for n being Element of NAT holds r2 < seq . n by A1, Def4;
take g = ((abs r1) + (abs r2)) + 1; :: thesis: ( 0 < g & ( for n being Element of NAT holds abs (seq . n) < g ) )
A4: 0 <= abs r1 by COMPLEX1:46;
0 <= abs r2 by COMPLEX1:46;
hence 0 < g by A4; :: thesis: for n being Element of NAT holds abs (seq . n) < g
let n be Element of NAT ; :: thesis: abs (seq . n) < g
r1 <= abs r1 by ABSVALUE:4;
then seq . n < abs r1 by A2, XXREAL_0:2;
then (seq . n) + 0 < (abs r1) + (abs r2) by COMPLEX1:46, XREAL_1:8;
then A5: seq . n < g by XREAL_1:8;
- (abs r2) <= r2 by ABSVALUE:4;
then - (abs r2) < seq . n by A3, XXREAL_0:2;
then (- (abs r1)) + (- (abs r2)) < 0 + (seq . n) by A4, XREAL_1:8;
then A6: ((- (abs r1)) - (abs r2)) + (- 1) < (seq . n) + 0 by XREAL_1:8;
((- (abs r1)) - (abs r2)) - 1 = - g ;
hence abs (seq . n) < g by A5, A6, Th9; :: thesis: verum

end;

given r being real number such that 0 < r and
A7: for n being Element of NAT holds abs (seq . n) < r ; :: thesis: seq is bounded
take r ; :: according to SEQ_2:def 5 :: thesis: for y being set st y in dom seq holds
abs (seq . y) < r
let y be set ; :: thesis: ( y in dom seq implies abs (seq . y) < r )
assume y in dom seq ; :: thesis: abs (seq . y) < r
then y is Element of NAT by FUNCT_2:def 1;
hence abs (seq . y) < r by A7; :: thesis: verum