theorem Th57: :: HERMITAN:57

for V being VectSp of F_Complex
for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V st Re (f . (v,v)) = 0 holds
f . (v,v) = 0. F_Complex