let v, w be Vector of V; :: according to BILINEAR:def 25 :: thesis: (- f) . (v,w) = (- f) . (w,v)
thus (- f) . (v,w) = - (f . (v,w)) by Def4
.= - (f . (w,v)) by Def25
.= (- f) . (w,v) by Def4 ; :: thesis: verum