consider f being non trivial V11() linear-Functional of the carrier of K, g being non trivial V11() linear-Functional of the carrier of K;
take FormFunctional f,g ; :: thesis:
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: