let X be non empty set ; :: thesis: for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions X,Y)
let Y be ComplexNormSpace; :: thesis: X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions X,Y)
X --> (0. Y) = 0. (C_VectorSpace_of_BoundedFunctions X,Y) by Th13
.= 0. (C_NormSpace_of_BoundedFunctions X,Y) ;
hence X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions X,Y) ; :: thesis: verum