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:10;
hence FunctionalFAF ((NulForm (V,W)),v) is cmplxhomogeneous ; :: thesis: verum