:: deftheorem Def22 defines i-shift HAHNBAN1:def 22 :
for V being non empty ModuleStr over F_Complex
for l, b₃ being RFunctional of V holds
( b₃ = i-shift l iff for v being Element of V holds b₃ . v = l . (i_FC * v) );