theorem :: HERMITAN:21

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