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