let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
let f be PartFunc of C,COMPLEX; :: thesis: ( |.f.| is bounded iff f is bounded )
A1: dom f = dom |.f.| by VALUED_1:def 11;
thus ( |.f.| is bounded implies f is bounded ) :: thesis: ( f is bounded implies |.f.| is bounded )
proof
assume |.f.| is bounded ; :: thesis: f is bounded
then consider r1 being Real such that
A2: for y being set st y in dom |.f.| holds
|.(|.f.| . y).| < r1 by COMSEQ_2:def 3;
now :: thesis: for y being set st y in dom f holds
not r1 <= |.(f . y).|
let y be set ; :: thesis: ( y in dom f implies not r1 <= |.(f . y).| )
assume A3: y in dom f ; :: thesis: not r1 <= |.(f . y).|
then |.(|.f.| . y).| < r1 by A1, A2;
then |.|.(f . y).|.| < r1 by A1, A3, VALUED_1:def 11;
hence not r1 <= |.(f . y).| ; :: thesis: verum
end;
hence f is bounded by COMSEQ_2:def 3; :: thesis: verum
end;
assume f is bounded ; :: thesis: |.f.| is bounded
then consider r2 being Real such that
A4: for y being set st y in dom f holds
|.(f . y).| < r2 by COMSEQ_2:def 3;
now :: thesis: ex r2 being Real st
for y being set st y in dom |.f.| holds
|.(|.f.| . y).| < r2
take r2 = r2; :: thesis: for y being set st y in dom |.f.| holds
|.(|.f.| . y).| < r2
let y be set ; :: thesis: ( y in dom |.f.| implies |.(|.f.| . y).| < r2 )
assume A5: y in dom |.f.| ; :: thesis: |.(|.f.| . y).| < r2
then |.|.(f . y).|.| < r2 by A1, A4;
hence |.(|.f.| . y).| < r2 by A5, VALUED_1:def 11; :: thesis: verum
end;
hence |.f.| is bounded by COMSEQ_2:def 3; :: thesis: verum