take NulForm (V,V) ; :: thesis: ( NulForm (V,V) is diagReR+0valued & NulForm (V,V) is hermitan & NulForm (V,V) is diagRvalued & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF & NulForm (V,V) is additiveFAF & NulForm (V,V) is cmplxhomogeneousFAF )
thus ( NulForm (V,V) is diagReR+0valued & NulForm (V,V) is hermitan & NulForm (V,V) is diagRvalued & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF & NulForm (V,V) is additiveFAF & NulForm (V,V) is cmplxhomogeneousFAF ) ; :: thesis: verum