theorem :: LOPBAN10:13

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