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