:: deftheorem defines bounded COMSEQ_2:def 3 :
for f being complex-valued Function holds
( f is bounded iff ex r being Real st
for y being set st y in dom f holds
|.(f . y).| < r );