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