take NulFrForm (V,W) ; :: thesis: ( NulFrForm (V,W) is additiveFAF & NulFrForm (V,W) is homogeneousFAF & NulFrForm (V,W) is additiveSAF & NulFrForm (V,W) is homogeneousSAF )
thus ( NulFrForm (V,W) is additiveFAF & NulFrForm (V,W) is homogeneousFAF & NulFrForm (V,W) is additiveSAF & NulFrForm (V,W) is homogeneousSAF ) ; :: thesis: verum