let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace holds the carrier of (product X) --> (0. Y) = 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
let Y be RealNormSpace; :: thesis: the carrier of (product X) --> (0. Y) = 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
the carrier of (product X) --> (0. Y) = 0. (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) by Th26
.= 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) ;
hence the carrier of (product X) --> (0. Y) = 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) ; :: thesis: verum