let v be Vector of V; :: according to BILINEAR:def 27 :: thesis: (a * f) . v,v = 0. K
thus (a * f) . v,v = a * (f . v,v) by Def4
.= a * (0. K) by Def27
.= 0. K by VECTSP_1:36 ; :: thesis: verum