:: deftheorem Def7 defines diagReR+0valued HERMITAN:def 7 :
for V being non empty ModuleStr over F_Complex
for f being Form of V,V holds
( f is diagReR+0valued iff for v being Vector of V holds 0 <= Re (f . (v,v)) );