consider f being non constant non trivial additive homogeneous 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