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

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