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