:: deftheorem defines PreNorms CSSPACE4:def 8 :
for X being non empty set
for Y being ComplexNormSpace
for u being Function of X, the carrier of Y holds PreNorms u = { ||.(u . t).|| where t is Element of X : verum } ;