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