:: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def 5 :
for X being non empty set
for Y being ComplexNormSpace
for b₃ being Subset of (ComplexVectSpace (X,Y)) holds
( b₃ = ComplexBoundedFunctions (X,Y) iff for x being set holds
( x in b₃ iff x is bounded Function of X, the carrier of Y ) );