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