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)
A1: C_VectorSpace_of_BoundedFunctions X,Y is Subspace of ComplexVectSpace X,Y by Th8, CSSPACE:13;
0. (ComplexVectSpace X,Y) = X --> (0. Y) by LOPBAN_1:def 3;
hence 0. (C_VectorSpace_of_BoundedFunctions X,Y) = X --> (0. Y) by A1, CLVECT_1:31; :: thesis: verum