:: deftheorem defines CtoR HAHNBAN1:def 21 :
for V being non empty ModuleStr over F_Complex
for l being RFunctional of V holds CtoR l = l;