:: deftheorem defines PreNorms DUALSP04:def 10 :
for X being RealUnitarySpace
for u being linear-Functional of X holds PreNorms u = { |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;