:: deftheorem Def10 defines quasinorm HERMITAN:def 10 :
for V being non empty ModuleStr over F_Complex
for f being Form of V,V
for b₃ being RFunctional of V holds
( b₃ = quasinorm f iff for v being Element of V holds b₃ . v = sqrt (signnorm (f,v)) );