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