:: deftheorem defines PreNorms C0SP1:def 16 :
for X being non empty set
for f being Function of X,REAL holds PreNorms f = { |.(f . x).| where x is Element of X : verum } ;