let v be Vector of V; :: according to BILINEAR:def 27 :: thesis: (NulForm V,V) . v,v = 0. K
thus (NulForm V,V) . v,v = 0. K by FUNCOP_1:85; :: thesis: verum