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 Th11

.= 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ;

hence X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; :: thesis: verum

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 Th11

.= 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ;

hence X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; :: thesis: verum