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