let X be non empty set ; :: thesis: for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
let Y be ComplexNormSpace; :: thesis: 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
( C_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of ComplexVectSpace (X,Y) & 0. (ComplexVectSpace (X,Y)) = X --> (0. Y) ) by Th7, CSSPACE:11, LOPBAN_1:def 3;
hence 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) by CLVECT_1:30; :: thesis: verum