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