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