let v be Vector of V; :: according to BILINEAR:def 27 :: thesis: (f + g) . v,v = 0. K
thus (f + g) . v,v = (f . v,v) + (g . v,v) by Def3
.= (0. K) + (g . v,v) by Def27
.= (0. K) + (0. K) by Def27
.= 0. K by RLVECT_1:def 7 ; :: thesis: verum