:: deftheorem defines PreNorms LOPBAN10:def 14 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for u being MultilinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } ;