theorem :: HERMITAN:29

for V, W being non empty ModuleStr over F_Complex
for f being Form of V,W holds (f *') *' = f