let f be real-valued Function; :: thesis: ( f is bounded iff ex r being Real st

for c being object st c in dom f holds

|.(f . c).| <= r )

thus ( f is bounded implies ex r being Real st

for c being object st c in dom f holds

|.(f . c).| <= r ) :: thesis: ( ex r being Real st

for c being object st c in dom f holds

|.(f . c).| <= r implies f is bounded )

|.(f . c).| <= r ; :: thesis: f is bounded

thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below_{1} being object holds

( not b_{1} in dom f or not f . b_{1} <= - (r + 1) )

let c be object ; :: thesis: ( not c in dom f or not f . c <= - (r + 1) )

assume c in dom f ; :: thesis: not f . c <= - (r + 1)

then |.(f . c).| < r + 1 by A9, XREAL_1:39;

then A11: - (r + 1) < - |.(f . c).| by XREAL_1:24;

- |.(f . c).| <= f . c by ABSVALUE:4;

hence not f . c <= - (r + 1) by A11, XXREAL_0:2; :: thesis: verum

for c being object st c in dom f holds

|.(f . c).| <= r )

thus ( f is bounded implies ex r being Real st

for c being object st c in dom f holds

|.(f . c).| <= r ) :: thesis: ( ex r being Real st

for c being object st c in dom f holds

|.(f . c).| <= r implies f is bounded )

proof

given r being Real such that A9:
for c being object st c in dom f holds
assume A1:
f is bounded
; :: thesis: ex r being Real st

for c being object st c in dom f holds

|.(f . c).| <= r

then consider r1 being Real such that

A2: for c being object st c in dom f holds

f . c < r1 by SEQ_2:def 1;

consider r2 being Real such that

A3: for c being object st c in dom f holds

r2 < f . c by A1, SEQ_2:def 2;

take g = |.r1.| + |.r2.|; :: thesis: for c being object st c in dom f holds

|.(f . c).| <= g

let c be object ; :: thesis: ( c in dom f implies |.(f . c).| <= g )

assume A4: c in dom f ; :: thesis: |.(f . c).| <= g

A5: 0 <= |.r2.| by COMPLEX1:46;

r1 <= |.r1.| by ABSVALUE:4;

then f . c <= |.r1.| by A2, A4, XXREAL_0:2;

then A6: (f . c) + 0 <= |.r1.| + |.r2.| by A5, XREAL_1:7;

A7: 0 <= |.r1.| by COMPLEX1:46;

- |.r2.| <= r2 by ABSVALUE:4;

then - |.r2.| <= f . c by A3, A4, XXREAL_0:2;

then A8: (- |.r1.|) + (- |.r2.|) <= 0 + (f . c) by A7, XREAL_1:7;

(- |.r1.|) + (- |.r2.|) = - g ;

hence |.(f . c).| <= g by A6, A8, ABSVALUE:5; :: thesis: verum

end;for c being object st c in dom f holds

|.(f . c).| <= r

then consider r1 being Real such that

A2: for c being object st c in dom f holds

f . c < r1 by SEQ_2:def 1;

consider r2 being Real such that

A3: for c being object st c in dom f holds

r2 < f . c by A1, SEQ_2:def 2;

take g = |.r1.| + |.r2.|; :: thesis: for c being object st c in dom f holds

|.(f . c).| <= g

let c be object ; :: thesis: ( c in dom f implies |.(f . c).| <= g )

assume A4: c in dom f ; :: thesis: |.(f . c).| <= g

A5: 0 <= |.r2.| by COMPLEX1:46;

r1 <= |.r1.| by ABSVALUE:4;

then f . c <= |.r1.| by A2, A4, XXREAL_0:2;

then A6: (f . c) + 0 <= |.r1.| + |.r2.| by A5, XREAL_1:7;

A7: 0 <= |.r1.| by COMPLEX1:46;

- |.r2.| <= r2 by ABSVALUE:4;

then - |.r2.| <= f . c by A3, A4, XXREAL_0:2;

then A8: (- |.r1.|) + (- |.r2.|) <= 0 + (f . c) by A7, XREAL_1:7;

(- |.r1.|) + (- |.r2.|) = - g ;

hence |.(f . c).| <= g by A6, A8, ABSVALUE:5; :: thesis: verum

|.(f . c).| <= r ; :: thesis: f is bounded

thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below

proof

take
- (r + 1)
; :: according to SEQ_2:def 2 :: thesis: for b
take
r + 1
; :: according to SEQ_2:def 1 :: thesis: for b_{1} being object holds

( not b_{1} in dom f or not r + 1 <= f . b_{1} )

let c be object ; :: thesis: ( not c in dom f or not r + 1 <= f . c )

assume c in dom f ; :: thesis: not r + 1 <= f . c

then A10: |.(f . c).| < r + 1 by A9, XREAL_1:39;

f . c <= |.(f . c).| by ABSVALUE:4;

hence not r + 1 <= f . c by A10, XXREAL_0:2; :: thesis: verum

end;( not b

let c be object ; :: thesis: ( not c in dom f or not r + 1 <= f . c )

assume c in dom f ; :: thesis: not r + 1 <= f . c

then A10: |.(f . c).| < r + 1 by A9, XREAL_1:39;

f . c <= |.(f . c).| by ABSVALUE:4;

hence not r + 1 <= f . c by A10, XXREAL_0:2; :: thesis: verum

( not b

let c be object ; :: thesis: ( not c in dom f or not f . c <= - (r + 1) )

assume c in dom f ; :: thesis: not f . c <= - (r + 1)

then |.(f . c).| < r + 1 by A9, XREAL_1:39;

then A11: - (r + 1) < - |.(f . c).| by XREAL_1:24;

- |.(f . c).| <= f . c by ABSVALUE:4;

hence not f . c <= - (r + 1) by A11, XXREAL_0:2; :: thesis: verum