theorem Th31: :: HERMITAN:31
for V, W being non empty ModuleStr over F_Complex
for f, g being Form of V,W holds (f + g) *' = (f *') + (g *')