let v be Vector of V; :: according to BILINEAR:def 13 :: thesis: FunctionalFAF ((NulForm (V,W)),v) is homogeneous

FunctionalFAF ((NulForm (V,W)),v) = 0Functional W by Th10;

hence FunctionalFAF ((NulForm (V,W)),v) is homogeneous ; :: thesis: verum

FunctionalFAF ((NulForm (V,W)),v) = 0Functional W by Th10;

hence FunctionalFAF ((NulForm (V,W)),v) is homogeneous ; :: thesis: verum