:: deftheorem Def23 defines prodReIm HAHNBAN1:def 23 :
for V being non empty ModuleStr over F_Complex
for l being Functional of (RealVS V)
for b₃ being Functional of V holds
( b₃ = prodReIm l iff for v being Element of V holds b₃ . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] );