let X be non empty set ; for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace
let Y be ComplexNormSpace; C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace
CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is ComplexLinearSpace
;
hence
C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace
by Th23, CSSPACE3:2; verum