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