let X be non empty set ; :: thesis: for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions X,Y is ComplexNormSpace
let Y be ComplexNormSpace; :: thesis: 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 Th26, CSSPACE3:4; :: thesis: verum