consider f being non trivial V11() linear-Functional of V, g being non trivial V11() 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