theorem :: HERMITAN:33

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