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