let v be Vector of V; :: according to BILINEAR:def 26 :: thesis: (- f) . (v,v) = 0. K

thus (- f) . (v,v) = - (f . (v,v)) by Def4

.= - (0. K) by Def26

.= 0. K by RLVECT_1:12 ; :: thesis: verum

thus (- f) . (v,v) = - (f . (v,v)) by Def4

.= - (0. K) by Def26

.= 0. K by RLVECT_1:12 ; :: thesis: verum