theorem :: CFUNCT_1:85

for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded ) by Lm3;