let Y be set ; :: thesis: for f being real-valued Function holds

( f | Y is bounded iff ex r being Real st

for c being object st c in Y /\ (dom f) holds

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

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

for c being object st c in Y /\ (dom f) holds

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

thus ( f | Y is bounded implies ex r being Real st

for c being object st c in Y /\ (dom f) holds

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

for c being object st c in Y /\ (dom f) holds

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

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

hence f | Y is bounded by A13; :: thesis: verum

( f | Y is bounded iff ex r being Real st

for c being object st c in Y /\ (dom f) holds

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

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

for c being object st c in Y /\ (dom f) holds

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

thus ( f | Y is bounded implies ex r being Real st

for c being object st c in Y /\ (dom f) holds

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

for c being object st c in Y /\ (dom f) holds

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

proof

given r being Real such that A11:
for c being object st c in Y /\ (dom f) holds
assume A1:
f | Y is bounded
; :: thesis: ex r being Real st

for c being object st c in Y /\ (dom f) holds

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

then consider r1 being Real such that

A2: for c being object st c in Y /\ (dom f) holds

f . c <= r1 by Th70;

consider r2 being Real such that

A3: for c being object st c in Y /\ (dom f) holds

r2 <= f . c by A1, Th71;

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

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

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

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

assume A5: c in Y /\ (dom f) ; :: thesis: |.(f . c).| <= g

f . c <= r1 by A2, A5;

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

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

r2 <= f . c by A3, A5;

then A8: - |.r2.| <= f . c by A7, XXREAL_0:2;

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

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

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

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

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

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

end;for c being object st c in Y /\ (dom f) holds

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

then consider r1 being Real such that

A2: for c being object st c in Y /\ (dom f) holds

f . c <= r1 by Th70;

consider r2 being Real such that

A3: for c being object st c in Y /\ (dom f) holds

r2 <= f . c by A1, Th71;

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

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

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

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

assume A5: c in Y /\ (dom f) ; :: thesis: |.(f . c).| <= g

f . c <= r1 by A2, A5;

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

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

r2 <= f . c by A3, A5;

then A8: - |.r2.| <= f . c by A7, XXREAL_0:2;

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

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

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

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

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

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

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

now :: thesis: for c being object st c in Y /\ (dom f) holds

- r <= f . c

then A13:
f | Y is bounded_below
by Th71;- r <= f . c

let c be object ; :: thesis: ( c in Y /\ (dom f) implies - r <= f . c )

assume c in Y /\ (dom f) ; :: thesis: - r <= f . c

then |.(f . c).| <= r by A11;

then A12: - r <= - |.(f . c).| by XREAL_1:24;

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

hence - r <= f . c by A12, XXREAL_0:2; :: thesis: verum

end;assume c in Y /\ (dom f) ; :: thesis: - r <= f . c

then |.(f . c).| <= r by A11;

then A12: - r <= - |.(f . c).| by XREAL_1:24;

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

hence - r <= f . c by A12, XXREAL_0:2; :: thesis: verum

now :: thesis: for c being object st c in Y /\ (dom f) holds

f . c <= r

then
f | Y is bounded_above
by Th70;f . c <= r

let c be object ; :: thesis: ( c in Y /\ (dom f) implies f . c <= r )

assume c in Y /\ (dom f) ; :: thesis: f . c <= r

then A14: |.(f . c).| <= r by A11;

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

hence f . c <= r by A14, XXREAL_0:2; :: thesis: verum

end;assume c in Y /\ (dom f) ; :: thesis: f . c <= r

then A14: |.(f . c).| <= r by A11;

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

hence f . c <= r by A14, XXREAL_0:2; :: thesis: verum

hence f | Y is bounded by A13; :: thesis: verum