let y be Vector of W; :: according to ZMODLAT1:def 30 :: thesis: FrFunctionalSAF ((NulFrForm (V,W)),y) is homogeneous
FrFunctionalSAF ((NulFrForm (V,W)),y) = 0FrFunctional V by HTh11;
hence FrFunctionalSAF ((NulFrForm (V,W)),y) is homogeneous ; :: thesis: verum