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