:: deftheorem Def4 defines bounded CSSPACE4:def 4 :
for X being non empty set
for Y being ComplexNormSpace
for IT being Function of X, the carrier of Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ) );