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

now

let y be set ; :: thesis: ( y in dom f implies not r1 <= |.(f . y).| )
assume A5: y in dom f ; :: thesis: not r1 <= |.(f . y).|
then |.(|.f.| . y).| < r1 by A1, A3;
then |.|.(f . y).|.| < r1 by A1, A5, VALUED_1:def 11;
hence not r1 <= |.(f . y).| ; :: thesis: verum

end;

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

end;

assume f is bounded ; :: thesis: |.f.| is bounded
then consider r2 being real number such that
A7: for y being set st y in dom f holds
|.(f . y).| < r2 by SEQ_2:def 5;

now

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 A8: y in dom |.f.| ; :: thesis: |.(|.f.| . y).| < r2
then |.|.(f . y).|.| < r2 by A1, A7;
hence |.(|.f.| . y).| < r2 by A8, VALUED_1:def 11; :: thesis: verum

end;

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