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 Th23, CSSPACE3:2; :: thesis: verum