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
P01: 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 P02: y in dom (Re f) ; :: thesis: abs ((Re f) . y) < r
then P03: y in dom f by COMSEQ_3:def 3;
abs (Re (f . y)) <= abs (f . y) by COMPLEX1:165;
then abs (Re (f . y)) < r by P01, P03, XXREAL_0:2;
hence abs ((Re f) . y) < r by P02, 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 P02: y in dom (Im f) ; :: thesis: abs ((Im f) . y) < r
then P03: y in dom f by COMSEQ_3:def 4;
abs (Im (f . y)) <= abs (f . y) by COMPLEX1:165;
then abs (Im (f . y)) < r by P01, P03, XXREAL_0:2;
hence abs ((Im f) . y) < r by P02, 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 P01: ( Re f is bounded & Im f is bounded ) ; :: thesis: f is bounded
then consider r1 being real number such that
P02: 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
P03: for y being set st y in dom (Im f) holds
abs ((Im f) . y) < r2 by P01, SEQ_2:def 5;

now

let y be set ; :: thesis: ( y in dom f implies abs (f . y) < r1 + r2 )
assume P04: y in dom f ; :: thesis: abs (f . y) < r1 + r2
then P05: y in dom (Re f) by COMSEQ_3:def 3;
then abs ((Re f) . y) < r1 by P02;
then P06: abs (Re (f . y)) < r1 by P05, COMSEQ_3:def 3;
P07: y in dom (Im f) by P04, COMSEQ_3:def 4;
then abs ((Im f) . y) < r2 by P03;
then P08: abs (Im (f . y)) < r2 by P07, COMSEQ_3:def 4;
P09: abs (f . y) <= (abs (Re (f . y))) + (abs (Im (f . y))) by COMPLEX1:164;
(abs (Re (f . y))) + (abs (Im (f . y))) < r1 + r2 by XREAL_1:10, P06, P08;
hence abs (f . y) < r1 + r2 by P09, XXREAL_0:2; :: thesis: verum

end;

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

end;