consider f being non trivial non constant homogeneous additive Functional of V;
take FormFunctional f,(f *' ) ; :: thesis: ( FormFunctional f,(f *' ) is diagReR+0valued & FormFunctional f,(f *' ) is hermitan & FormFunctional f,(f *' ) is diagRvalued & FormFunctional f,(f *' ) is additiveSAF & FormFunctional f,(f *' ) is homogeneousSAF & FormFunctional f,(f *' ) is additiveFAF & FormFunctional f,(f *' ) is cmplxhomogeneousFAF & not FormFunctional f,(f *' ) is constant & not FormFunctional f,(f *' ) is trivial )
thus ( FormFunctional f,(f *' ) is diagReR+0valued & FormFunctional f,(f *' ) is hermitan & FormFunctional f,(f *' ) is diagRvalued & FormFunctional f,(f *' ) is additiveSAF & FormFunctional f,(f *' ) is homogeneousSAF & FormFunctional f,(f *' ) is additiveFAF & FormFunctional f,(f *' ) is cmplxhomogeneousFAF & not FormFunctional f,(f *' ) is constant & not FormFunctional f,(f *' ) is trivial ) ; :: thesis: verum