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