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