set f = the non trivial V17() linear-Functional of V;

set g = the non trivial V17() linear-Functional of W;

take FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) ; :: thesis: ( not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is trivial & not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is constant & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveSAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousSAF )

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

set g = the non trivial V17() linear-Functional of W;

take FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) ; :: thesis: ( not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is trivial & not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is constant & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveSAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousSAF )

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