let seq be Real_Sequence; :: thesis: ( seq is bounded iff ex r being Real st
( 0 < r & ( for n being Nat holds |.(seq . n).| < r ) ) )
thus ( seq is bounded implies ex r being Real st
( 0 < r & ( for n being Nat holds |.(seq . n).| < r ) ) ) :: thesis: ( ex r being Real st
( 0 < r & ( for n being Nat holds |.(seq . n).| < r ) ) implies seq is bounded )

proof

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

end;

given r being Real such that 0 < r and
A7: for n being Nat holds |.(seq . n).| < r ; :: thesis: seq is bounded
take r ; :: according to COMSEQ_2:def 3 :: thesis: for b₁ being set holds
( not b₁ in dom seq or not r <= |.(seq . b₁).| )
let y be set ; :: thesis: ( not y in dom seq or not r <= |.(seq . y).| )
assume y in dom seq ; :: thesis: not r <= |.(seq . y).|
then y is Element of NAT by FUNCT_2:def 1;
hence not r <= |.(seq . y).| by A7; :: thesis: verum