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
|.((abs f) . y).| < r1 ;
take r1 ; :: according to COMSEQ_2:def 3 :: thesis: for b₁ being set holds
( not b₁ in dom f or not r1 <= |.(f . b₁).| )
let y be set ; :: thesis: ( not y in dom f or not r1 <= |.(f . y).| )
assume A3: y in dom f ; :: thesis: not r1 <= |.(f . y).|
then |.((abs 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;

given r1 being Real such that A4: for y being set st y in dom f holds
|.(f . y).| < r1 ; :: according to COMSEQ_2:def 3 :: thesis: |.f.| is bounded

now :: thesis: ex r1 being Real st
for y being set st y in dom |.f.| holds
|.((abs f) . y).| < r1

take r1 = r1; :: thesis: for y being set st y in dom |.f.| holds
|.((abs f) . y).| < r1
let y be set ; :: thesis: ( y in dom |.f.| implies |.((abs f) . y).| < r1 )
assume A5: y in dom |.f.| ; :: thesis: |.((abs f) . y).| < r1
then |.|.(f . y).|.| < r1 by A1, A4;
hence |.((abs f) . y).| < r1 by A5, VALUED_1:def 11; :: thesis: verum

end;

hence |.f.| is bounded ; :: thesis: verum