theorem :: HERMITAN:34

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