theorem Th31: :: LOPBAN10:44

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