let v be Vector of V; :: according to ZMODLAT1:def 29 :: thesis: FrFunctionalFAF ((NulFrForm (V,W)),v) is homogeneous
FrFunctionalFAF ((NulFrForm (V,W)),v) = 0FrFunctional W by HTh10;
hence FrFunctionalFAF ((NulFrForm (V,W)),v) is homogeneous ; :: thesis: verum