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