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