theorem Th23: :: HAHNBAN1:25

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