theorem :: HERMITAN:16

for V being non empty ModuleStr over F_Complex
for f being Functional of V holds (f *') *' = f ;