theorem Th21: :: HAHNBAN1:23

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