:: deftheorem Def18 defines projRe HAHNBAN1:def 18 :
for V being non empty ModuleStr over F_Complex
for l being Functional of V
for b₃ being Functional of (RealVS V) holds
( b₃ = projRe l iff for i being Element of V holds b₃ . i = Re (l . i) );