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 )

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;

( |.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
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;

end;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).|

hence
f is bounded
by COMSEQ_2:def 3; :: thesis: verumnot 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;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

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

hence
|.f.| is bounded
by COMSEQ_2:def 3; :: thesis: verumfor 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;|.(|.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