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
A2: 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 K1(f) or not r1 <= abs (f . b₁) )
let y be set ; :: thesis: ( not y in K1(f) or not r1 <= abs (f . y) )
assume A3: y in dom f ; :: thesis: not r1 <= abs (f . y)
then abs (|.f.| . y) < r1 by A1, A2;
then abs |.(f . y).| < r1 by A1, A3, VALUED_1:def 11;
hence not r1 <= abs (f . y) ; :: thesis: verum

end;

given r1 being real number such that A4: 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 A5: y in dom |.f.| ; :: thesis: abs (|.f.| . y) < r1
then abs |.(f . y).| < r1 by A1, A4;
hence abs (|.f.| . y) < r1 by A5, VALUED_1:def 11; :: thesis: verum

end;

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