theorem :: HAHNBAN1:26

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