for V being non empty ModuleStr over F_Complex
for p being RFunctional of V holds p is Functional of (RealVS V)