set f = the non trivial non constant homogeneous additive Functional of V;
take the non trivial non constant homogeneous additive Functional of V *' ; :: thesis: ( the non trivial non constant homogeneous additive Functional of V *' is additive & the non trivial non constant homogeneous additive Functional of V *' is cmplxhomogeneous & not the non trivial non constant homogeneous additive Functional of V *' is constant & not the non trivial non constant homogeneous additive Functional of V *' is trivial )
thus ( the non trivial non constant homogeneous additive Functional of V *' is additive & the non trivial non constant homogeneous additive Functional of V *' is cmplxhomogeneous & not the non trivial non constant homogeneous additive Functional of V *' is constant & not the non trivial non constant homogeneous additive Functional of V *' is trivial ) ; :: thesis: verum