theorem Th45: :: HERMITAN:45

for V being VectSp of F_Complex
for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V holds |.(f . (v,w)).| ^2 <= (signnorm (f,v)) * (signnorm (f,w))