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