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)
; ( 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 )
; verum