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

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