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