let y be Vector of W; :: according to BILINEAR:def 14 :: thesis: FunctionalSAF ((NulForm (V,W)),y) is homogeneous

FunctionalSAF ((NulForm (V,W)),y) = 0Functional V by Th11;

hence FunctionalSAF ((NulForm (V,W)),y) is homogeneous ; :: thesis: verum

FunctionalSAF ((NulForm (V,W)),y) = 0Functional V by Th11;

hence FunctionalSAF ((NulForm (V,W)),y) is homogeneous ; :: thesis: verum