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 )

proof

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;

now :: thesis: for y being set st y in dom (Re f) holds
|.((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;

hence Re f is bounded by COMSEQ_2:def 3; :: thesis: Im f is bounded

now :: thesis: for y being set st y in dom (Im f) holds
|.((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;

hence Im f is bounded by COMSEQ_2:def 3; :: thesis: verum

end;

thus ( Re f is bounded & Im f is bounded implies f is bounded ) :: 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;

now :: thesis: for y being set st y in dom f holds
|.(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;

hence f is bounded by COMSEQ_2:def 3; :: thesis: verum

end;