consider g being non constant non trivial additive cmplxhomogeneous Functional of W;
consider f being non constant non trivial additive homogeneous Functional of V;
take FormFunctional f,g ; :: thesis: ( FormFunctional f,g is additiveSAF & FormFunctional f,g is homogeneousSAF & FormFunctional f,g is additiveFAF & FormFunctional f,g is cmplxhomogeneousFAF & not FormFunctional f,g is constant & not FormFunctional f,g is trivial )
thus ( FormFunctional f,g is additiveSAF & FormFunctional f,g is homogeneousSAF & FormFunctional f,g is additiveFAF & FormFunctional f,g is cmplxhomogeneousFAF & not FormFunctional f,g is constant & not FormFunctional f,g is trivial ) ; :: thesis: verum