theorem Th28: :: HERMITAN:28

for V being non empty ModuleStr over F_Complex
for f being Functional of V
for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2