:: deftheorem Def19 defines projIm HAHNBAN1:def 19 :
for V being non empty ModuleStr over F_Complex
for l being Functional of V
for b₃ being Functional of (RealVS V) holds
( b₃ = projIm l iff for i being Element of V holds b₃ . i = Im (l . i) );