let v be Vector of V; :: according to HERMITAN:def 4 :: thesis: FunctionalFAF (NulForm V,W),v is cmplxhomogeneous
FunctionalFAF (NulForm V,W),v = 0Functional W by BILINEAR:11;
hence FunctionalFAF (NulForm V,W),v is cmplxhomogeneous ; :: thesis: verum