let v be Vector of V; :: according to BILINEAR:def 27 :: thesis: (- f) . v,v = 0. K
thus (- f) . v,v = - (f . v,v) by Def5
.= - (0. K) by Def27
.= 0. K by RLVECT_1:25 ; :: thesis: verum