:: deftheorem Def3 defines Multilinear LOPBAN10:def 3 :
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for f being Function of (product X),Y holds
( f is Multilinear iff for i being Element of dom X
for x being Element of (product X) holds f * (reproj (i,x)) is LinearOperator of (X . i),Y );