theorem Th25: :: HAHNBAN1:27

for V being VectSp of F_Complex
for l being linear-Functional of (RealVS V) holds prodReIm l is linear-Functional of V