let v be Vector of V; :: according to BILINEAR:def 26 :: thesis: (f + g) . (v,v) = 0. K
thus (f + g) . (v,v) = (f . (v,v)) + (g . (v,v)) by Def2
.= (0. K) + (g . (v,v)) by Def26
.= (0. K) + (0. K) by Def26
.= 0. K by RLVECT_1:def 4 ; :: thesis: verum