:: deftheorem Def1 defines cmplxhomogeneous HERMITAN:def 1 :
for V being non empty ModuleStr over F_Complex
for f being Functional of V holds
( f is cmplxhomogeneous iff for v being Vector of V
for a being Scalar of holds f . (a * v) = (a *') * (f . v) );