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