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 number such that
A1: for y being set st y in dom f holds
abs (f . y) < r by SEQ_2:def 5;

now

let y be set ; :: thesis: ( y in dom (Re f) implies abs ((Re f) . y) < r )
assume A2: y in dom (Re f) ; :: thesis: abs ((Re f) . y) < r
then A3: y in dom f by COMSEQ_3:def 3;
abs (Re (f . y)) <= abs (f . y) by COMPLEX1:79;
then abs (Re (f . y)) < r by A1, A3, XXREAL_0:2;
hence abs ((Re f) . y) < r by A2, COMSEQ_3:def 3; :: thesis: verum

end;

hence Re f is bounded by SEQ_2:def 5; :: thesis: Im f is bounded

now

let y be set ; :: thesis: ( y in dom (Im f) implies abs ((Im f) . y) < r )
assume A4: y in dom (Im f) ; :: thesis: abs ((Im f) . y) < r
then A5: y in dom f by COMSEQ_3:def 4;
abs (Im (f . y)) <= abs (f . y) by COMPLEX1:79;
then abs (Im (f . y)) < r by A1, A5, XXREAL_0:2;
hence abs ((Im f) . y) < r by A4, COMSEQ_3:def 4; :: thesis: verum

end;

hence Im f is bounded by SEQ_2:def 5; :: 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 number such that
A7: for y being set st y in dom (Re f) holds
abs ((Re f) . y) < r1 by SEQ_2:def 5;
consider r2 being real number such that
A8: for y being set st y in dom (Im f) holds
abs ((Im f) . y) < r2 by A6, SEQ_2:def 5;

now

let y be set ; :: thesis: ( y in dom f implies abs (f . y) < r1 + r2 )
assume A9: y in dom f ; :: thesis: abs (f . y) < r1 + r2
then A10: y in dom (Re f) by COMSEQ_3:def 3;
then abs ((Re f) . y) < r1 by A7;
then A11: abs (Re (f . y)) < r1 by A10, COMSEQ_3:def 3;
A12: y in dom (Im f) by A9, COMSEQ_3:def 4;
then abs ((Im f) . y) < r2 by A8;
then A13: abs (Im (f . y)) < r2 by A12, COMSEQ_3:def 4;
A14: abs (f . y) <= (abs (Re (f . y))) + (abs (Im (f . y))) by COMPLEX1:78;
(abs (Re (f . y))) + (abs (Im (f . y))) < r1 + r2 by A11, A13, XREAL_1:8;
hence abs (f . y) < r1 + r2 by A14, XXREAL_0:2; :: thesis: verum

end;

hence f is bounded by SEQ_2:def 5; :: thesis: verum

end;