theorem Th26: :: LOPBAN10:32

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y)