for V being non empty ModuleStr over F_Complex
for f being Functional of V
for a being Scalar of holds (a * f) *' = (a *') * (f *')