let v be Vector of V; :: according to BILINEAR:def 26 :: thesis: (a * f) . (v,v) = 0. K
thus (a * f) . (v,v) = a * (f . (v,v)) by Def3
.= a * (0. K) by Def26
.= 0. K ; :: thesis: verum