consider g being non trivial non constant additive cmplxhomogeneous Functional of W;
consider f being non trivial non constant homogeneous additive 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