:: deftheorem defines PreNorms LOPBAN_9:def 7 :
for X, Y, Z being RealNormSpace
for u being BilinearOperator of X,Y,Z holds PreNorms u = { ||.(u . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) } ;