let y be Vector of W; :: according to BILINEAR:def 13 :: thesis: FunctionalSAF (NulForm V,W),y is additive
FunctionalSAF (NulForm V,W),y = 0Functional V by Th12;
hence FunctionalSAF (NulForm V,W),y is additive ; :: thesis: verum