let v be Vector of V; :: according to BILINEAR:def 14 :: thesis: FunctionalFAF (NulForm V,W),v is homogeneous
FunctionalFAF (NulForm V,W),v = 0Functional W by Th11;
hence FunctionalFAF (NulForm V,W),v is homogeneous ; :: thesis: verum