let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y)
let Y be RealNormSpace; :: thesis: 0. (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y)
A1: 0. (R_VectorSpace_of_MultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y) by Th18;
R_VectorSpace_of_BoundedMultilinearOperators (X,Y) is Subspace of R_VectorSpace_of_MultilinearOperators (X,Y) by RSSPACE:11;
hence 0. (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y) by A1, RLSUB_1:11; :: thesis: verum