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