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