:: deftheorem Def6 defines MultilinearOperators LOPBAN10:def 4 :
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for b₃ being Subset of (RealVectSpace ( the carrier of (product X),Y)) holds
( b₃ = MultilinearOperators (X,Y) iff for x being set holds
( x in b₃ iff x is MultilinearOperator of X,Y ) );