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