let y be Vector of ; :: 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