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