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