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