:: deftheorem defines QcFunctional HERMITAN:def 3 :
for V being VectSp of F_Complex
for f being antilinear-Functional of V holds QcFunctional f = QFunctional (f,(Ker (f *')));