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 ;
hence |.((Re f) . y).| < r by ; :: 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 ;
hence |.((Im f) . y).| < r by ; :: 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 ;
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 ;
A12: y in dom (Im f) by ;
then |.((Im f) . y).| < r2 by A8;
then A13: |.(Im (f . y)).| < r2 by ;
A14: |.(f . y).| <= |.(Re (f . y)).| + |.(Im (f . y)).| by COMPLEX1:78;
|.(Re (f . y)).| + |.(Im (f . y)).| < r1 + r2 by ;
hence |.(f . y).| < r1 + r2 by ; :: thesis: verum
end;
hence f is bounded by COMSEQ_2:def 3; :: thesis: verum
end;