theorem Th41: :: HERMITAN:41

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex
for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V holds
( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )