let f be PartFunc of REAL,COMPLEX; :: thesis: ( f is bounded iff ( Re f is bounded & Im f is bounded ) )

thus ( f is bounded implies ( Re f is bounded & Im f is bounded ) ) :: thesis: ( Re f is bounded & Im f is bounded implies f is bounded )

thus ( f is bounded implies ( Re f is bounded & Im f is bounded ) ) :: thesis: ( Re f is bounded & Im f is bounded implies f is bounded )

proof

thus
( Re f is bounded & Im f is bounded implies f is bounded )
:: thesis: verum
assume
f is bounded
; :: thesis: ( Re f is bounded & Im f is bounded )

then consider r being Real such that

A1: for y being set st y in dom f holds

|.(f . y).| < r by COMSEQ_2:def 3;

end;then consider r being Real such that

A1: for y being set st y in dom f holds

|.(f . y).| < r by COMSEQ_2:def 3;

now :: thesis: for y being set st y in dom (Re f) holds

|.((Re f) . y).| < r

hence
Re f is bounded
by COMSEQ_2:def 3; :: thesis: Im f is bounded |.((Re f) . y).| < r

let y be set ; :: thesis: ( y in dom (Re f) implies |.((Re f) . y).| < r )

assume A2: y in dom (Re f) ; :: thesis: |.((Re f) . y).| < r

then A3: y in dom f by COMSEQ_3:def 3;

|.(Re (f . y)).| <= |.(f . y).| by COMPLEX1:79;

then |.(Re (f . y)).| < r by A1, A3, XXREAL_0:2;

hence |.((Re f) . y).| < r by A2, COMSEQ_3:def 3; :: thesis: verum

end;assume A2: y in dom (Re f) ; :: thesis: |.((Re f) . y).| < r

then A3: y in dom f by COMSEQ_3:def 3;

|.(Re (f . y)).| <= |.(f . y).| by COMPLEX1:79;

then |.(Re (f . y)).| < r by A1, A3, XXREAL_0:2;

hence |.((Re f) . y).| < r by A2, COMSEQ_3:def 3; :: thesis: verum

now :: thesis: for y being set st y in dom (Im f) holds

|.((Im f) . y).| < r

hence
Im f is bounded
by COMSEQ_2:def 3; :: thesis: verum|.((Im f) . y).| < r

let y be set ; :: thesis: ( y in dom (Im f) implies |.((Im f) . y).| < r )

assume A4: y in dom (Im f) ; :: thesis: |.((Im f) . y).| < r

then A5: y in dom f by COMSEQ_3:def 4;

|.(Im (f . y)).| <= |.(f . y).| by COMPLEX1:79;

then |.(Im (f . y)).| < r by A1, A5, XXREAL_0:2;

hence |.((Im f) . y).| < r by A4, COMSEQ_3:def 4; :: thesis: verum

end;assume A4: y in dom (Im f) ; :: thesis: |.((Im f) . y).| < r

then A5: y in dom f by COMSEQ_3:def 4;

|.(Im (f . y)).| <= |.(f . y).| by COMPLEX1:79;

then |.(Im (f . y)).| < r by A1, A5, XXREAL_0:2;

hence |.((Im f) . y).| < r by A4, COMSEQ_3:def 4; :: thesis: verum

proof

assume A6:
( Re f is bounded & Im f is bounded )
; :: thesis: f is bounded

then consider r1 being Real such that

A7: for y being set st y in dom (Re f) holds

|.((Re f) . y).| < r1 by COMSEQ_2:def 3;

consider r2 being Real such that

A8: for y being set st y in dom (Im f) holds

|.((Im f) . y).| < r2 by A6, COMSEQ_2:def 3;

end;then consider r1 being Real such that

A7: for y being set st y in dom (Re f) holds

|.((Re f) . y).| < r1 by COMSEQ_2:def 3;

consider r2 being Real such that

A8: for y being set st y in dom (Im f) holds

|.((Im f) . y).| < r2 by A6, COMSEQ_2:def 3;

now :: thesis: for y being set st y in dom f holds

|.(f . y).| < r1 + r2

hence
f is bounded
by COMSEQ_2:def 3; :: thesis: verum|.(f . y).| < r1 + r2

let y be set ; :: thesis: ( y in dom f implies |.(f . y).| < r1 + r2 )

assume A9: y in dom f ; :: thesis: |.(f . y).| < r1 + r2

then A10: y in dom (Re f) by COMSEQ_3:def 3;

then |.((Re f) . y).| < r1 by A7;

then A11: |.(Re (f . y)).| < r1 by A10, COMSEQ_3:def 3;

A12: y in dom (Im f) by A9, COMSEQ_3:def 4;

then |.((Im f) . y).| < r2 by A8;

then A13: |.(Im (f . y)).| < r2 by A12, COMSEQ_3:def 4;

A14: |.(f . y).| <= |.(Re (f . y)).| + |.(Im (f . y)).| by COMPLEX1:78;

|.(Re (f . y)).| + |.(Im (f . y)).| < r1 + r2 by A11, A13, XREAL_1:8;

hence |.(f . y).| < r1 + r2 by A14, XXREAL_0:2; :: thesis: verum

end;assume A9: y in dom f ; :: thesis: |.(f . y).| < r1 + r2

then A10: y in dom (Re f) by COMSEQ_3:def 3;

then |.((Re f) . y).| < r1 by A7;

then A11: |.(Re (f . y)).| < r1 by A10, COMSEQ_3:def 3;

A12: y in dom (Im f) by A9, COMSEQ_3:def 4;

then |.((Im f) . y).| < r2 by A8;

then A13: |.(Im (f . y)).| < r2 by A12, COMSEQ_3:def 4;

A14: |.(f . y).| <= |.(Re (f . y)).| + |.(Im (f . y)).| by COMPLEX1:78;

|.(Re (f . y)).| + |.(Im (f . y)).| < r1 + r2 by A11, A13, XREAL_1:8;

hence |.(f . y).| < r1 + r2 by A14, XXREAL_0:2; :: thesis: verum