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