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 )
F: 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
G: for y being set st y in dom |.f.| holds
abs (|.f.| . y) < r1 by SEQ_2:def 5;
take r1 ; :: according to SEQ_2:def 5 :: thesis: for b₁ being set holds
( not b₁ in dom f or not r1 <= abs (f . b₁) )
let y be set ; :: thesis: ( not y in dom f or not r1 <= abs (f . y) )
assume Z: y in dom f ; :: thesis: not r1 <= abs (f . y)
then abs (|.f.| . y) < r1 by F, G;
then abs |.(f . y).| < r1 by F, Z, VALUED_1:def 11;
hence abs (f . y) < r1 ; :: thesis: verum

end;

given r1 being real number such that G: for y being set st y in dom f holds
abs (f . y) < r1 ; :: according to SEQ_2:def 5 :: thesis: |.f.| is bounded

now

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 Z: y in dom |.f.| ; :: thesis: abs (|.f.| . y) < r1
then abs |.(f . y).| < r1 by F, G;
hence abs (|.f.| . y) < r1 by Z, VALUED_1:def 11; :: thesis: verum

end;

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