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

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