theorem :: LOPBAN10:14

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