theorem Th58: :: HERMITAN:58

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds
v = 0. V